The weakest precondition calculus: Recursion and duality

DOI10.1007/BF01213603zbMath0816.68081OpenAlexW2012569382WikidataQ56504619 ScholiaQ56504619MaRDI QIDQ1346768

Marcello M. Bonsangue, Joost N. Kok

Publication date: 9 April 1995

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

Full work available at URL: https://doi.org/10.1007/bf01213603

zbMATH Keywords

refinementdenotational semanticsEgli-Milner power domainSmyth power domain

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55)

Related Items (5)

A fixpoint theory for non-monotonic parallelism ⋮ The weakest precondition calculus: Recursion and duality ⋮ Generic weakest precondition semantics from monads enriched with order ⋮ Symbolic execution formally explained ⋮ Coordinating action systems

Cites Work

• A theoretical basis for stepwise refinement and the programming calculus
• A simple fixpoint argument without the restriction to continuity
• Predicate-transformer semantics of general recursion
• On correct refinement of programs
• A characterization of weakest preconditions
• Power domains
• The weakest precondition calculus: Recursion and duality
• Countable nondeterminism and random assignment
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: The weakest precondition calculus: Recursion and duality