|
|||||
|
|
Safety and progress of recursive procedures |
|
| Authors: | Wim H. Hesselink |
| Affiliation: | (1) Department of Computing Science, Rijksuniversiteit Groningen, Groningen, The Netherlands;(2) Department of Computer Science, Rijksuniversiteit Groningen, PO Box 800, 9700 AV Groningen, The Netherlands |
| Abstract: | Temporal weakest precondions are introduced for calculational reasoning about the states encountered during execution of not-necessarily terminating recursive procedures. The formalism can distinguish error from useful nontermination. The precondition functions are constructed in a new and more elegant way. Healthiness laws are discussed briefly. Proof rules are introduced that enable calculational proofs of various safety and progress properties. The construction of the precondition functions is justified in an Appendix that provides the operational semantics.Dedicated to the memory of Jan van de Snepscheut |
| Keywords: | Predicate transformers Weakest preconditions Recursive procedures Operational semantics Proof rules Safety Progress |
| 本文献已被 SpringerLink 等数据库收录！ | |