Abstract
Two relations of the weakest precondition function are given. The first defines the sequential execution of two program statements. The second defines concurrent execution of two program statements in terms of buffering range variables and the relation for sequential execution. The statement types of the language KL-1 are given along with their operational semantics. A weakest precondition function is defined for each of these statement types. Finally it is shown, by using the sequential and concurrent relations, and the weakest precondition functions defined, how programs written with simple variables using the constructs of KL-1 can be demonstrated to be logically correct.
| Original language | English (US) |
|---|---|
| Title of host publication | Unknown Host Publication Title |
| Place of Publication | New York, NY |
| Publisher | IEEE |
| Pages | 635-639 |
| Number of pages | 5 |
| State | Published - 1800 |
| Externally published | Yes |
| Event | COMPSAC '77, IEEE Comput Soc Int Comput Software & Appl Conf, 1st, Proc - Chicago, IL, USA Duration: Nov 8 1977 → Nov 11 1977 |
Other
| Other | COMPSAC '77, IEEE Comput Soc Int Comput Software & Appl Conf, 1st, Proc |
|---|---|
| City | Chicago, IL, USA |
| Period | 11/8/77 → 11/11/77 |
ASJC Scopus subject areas
- Engineering(all)