Specifying the Semantics of while Programs: A Tutorial and Critique of a Paper by Hoare and Lauer

DOI10.1145/357146.357151zbMath0471.68007OpenAlexW1978078271MaRDI QIDQ3925146

Albert R. Meyer, Irene Greif

Publication date: 1981

Published in: ACM Transactions on Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/357146.357151

zbMATH Keywords

functionalspredicate transformerspartial correctnessdeductive systemsweakest preconditionsemantics of programming languagespredicatesprogram syntax

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) General topics in the theory of software (68N01)

Related Items

Expressing program looping in regular dynamic logic, Some applications of topology to program semantics, Semantics of algorithmic languages, A logical analysis of aliasing in imperative higher-order functions, Expressiveness and the completeness of Hoare's logic, The axiomatic semantics of programs based on Hoare's logic