Predicate transformers for recursive procedures with local variables

DOI10.1007/S001659970002MaRDI QIDQ1578396zbMATH OpenOpenAlexFDO

Authors W. H. Hesselink

Publication date 27 August 2000

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://pure.rug.nl/ws/files/3160928/1999FormAspCompHesselink2.pdf

zbMATH Keywords

imperative languageprecondition semantics of recursive procedures

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55)

Recommendations

• Predicate-transformer semantics of general recursion
• A general proof rule for procedures in predicate transformer semantics
• Proof rules for recursive procedures
• Safety and progress of recursive procedures

Cited in

(8)

• Alternating states for dual nondeterminism in imperative programming
• Frame rule for mutually recursive procedures manipulating pointers
• Safety and progress of recursive procedures
• Command algebras, recursion and program transformation
• Predicate-transformer semantics of general recursion
• Predicate transformer semantics of a higher-order imperative language with record subtyping
• Verifying and generating WP transformers for procedures on complex data
• Calculating with procedure calls

This page was built for publication: Predicate transformers for recursive procedures with local variables

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1578396)