Command Algebras, Recursion and Program TransformationHesselink, W. H., 1990, In : Formal Aspects of Computing. 2, 45 p.
Research output: Contribution to journal › Article › Academic
Dijkstra's language of guarded commands is extended with recursion and transformed into algebra. The semantics is expressed in terms of weakest preconditions and weakest liberal preconditions. Extreme fixed points are used to deal with recursion. Unbounded nondeterminacy is allowed. The algebraic setting enables us to develop efficient transformation rules for recursive procedures. The main result is an algebraic version of the rule of computational induction. In this version, certain parts of the programs are restricted to finite nondeterminacy. It is shown that without this restriction the rule would not be valid. Some applications of the rule are presented. In particular, we prove the correctness of an iterative stack implementation of a class of simple recursive procedures.
|Number of pages||45|
|Journal||Formal Aspects of Computing|
|Publication status||Published - 1990|
- Weakest precondition, Stack, Semantics, Semantic equivalence, Recursive procedure (or recursion), Program transformation, Nondeterminacy/nondeterminism, Lattice, Fixpoint, Computational induction, Command algebra
No data available