Command Algebras, Recursion and Program Transformation

Hesselink, W. H., 1990, In : Formal Aspects of Computing. 2, 45 p.

Research output: Contribution to journalArticleAcademic

Copy link to clipboard


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.
Original languageEnglish
Number of pages45
JournalFormal Aspects of Computing
Publication statusPublished - 1990


  • Weakest precondition, Stack, Semantics, Semantic equivalence, Recursive procedure (or recursion), Program transformation, Nondeterminacy/nondeterminism, Lattice, Fixpoint, Computational induction, Command algebra

Download statistics

No data available

ID: 3360996