Abstract
Dijkstra's predicate transformer for specifying the semantics of guarded commands set and proving the total correcness of a program is generalized to a programming language with the go to statement. The concept of general predicate transformer and its properties are introduced. We explore the approach of proving the correctness - preserving property of some common program transformations that are used in the compiling process.
| Original language | English |
|---|---|
| Pages (from-to) | 35-57 |
| Number of pages | 23 |
| Journal | Acta Informatica |
| Volume | 20 |
| Issue number | 1 |
| DOIs | |
| State | Published - Oct 1983 |