Command algebras, recursion and program transformation
- 1 March 1990
- journal article
- Published by Association for Computing Machinery (ACM) in Formal Aspects of Computing
- Vol. 2 (1) , 60-104
- https://doi.org/10.1007/bf01888217
Abstract
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.Keywords
This publication has 15 references indexed in Scilit:
- Modalities of NondeterminacyPublished by Springer Nature ,1990
- A generalization of Dijkstra's calculusACM Transactions on Programming Languages and Systems, 1989
- Interpretations of recursion under unbounded nondeterminacyTheoretical Computer Science, 1988
- Data refinement by miraclesInformation Processing Letters, 1988
- Data Refinement by MiraclesPublished by Springer Nature ,1988
- On the consistency of Koomen's Fair Abstraction RuleTheoretical Computer Science, 1987
- Ten Years of Hoare's Logic: A Survey—Part IACM Transactions on Programming Languages and Systems, 1981
- Some Properties of Predicate TransformersJournal of the ACM, 1978
- IntroductionPublished by Springer Nature ,1971
- Procedures and parameters: An axiomatic approachLecture Notes in Mathematics, 1971