Representing WP semantics in Isabelle/ZF

DOI10.1007/3-540-48256-3_16MaRDI QIDQ4945210zbMATH OpenFDO

Authors Mark Staples

Publication date 23 March 2000

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-48256-3_16

zbMATH Keywords

program refinement language

Mathematics Subject Classification ID

Recommendations

• A Weakest Precondition Semantics for Z
• Refinement concepts formalised in higher order logic
• scientific article; zbMATH DE number 1927431
• Expression refinement in higher order logic
• scientific article; zbMATH DE number 1863389

Cited in

(3)

• Isabelle/ZF
• Formalization of Refinement Calculus for Reactive Systems
• Algebra of Monotonic Boolean Transformers

Describes a project that uses

Uses Software

• Isabelle

This page was built for publication: Representing WP semantics in Isabelle/ZF

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