Angelic nondeterminism in the unifying theories of programming

DOI10.1007/s00165-006-0001-8zbMath1105.68012MaRDI QIDQ851128

Ana Cavalcanti, J. C. P. Woodcock, Steve Dunne

Publication date: 17 November 2006

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

Full work available at URL: https://research.tees.ac.uk/ws/files/6483463/58302.pdf

zbMATH Keywords

relations; semantics; refinement; predicate transformers

Mathematics Subject Classification ID

68N01: General topics in the theory of software

Related Items

Multirelations with infinite computations, Mechanised support for sound refinement tactics, Modelling higher-order dual nondeterminacy, Unifying theories in ProofPower-Z, Simulink Timed Models for Program Verification

Uses Software

• ZRC
• Circus

Cites Work

• A refinement strategy for Circus
• Data refinement by calculation
• Duality in specification languages: A lattice-theoretical approach
• The weakest prespecification
• Data refinement of predicate transformers
• Combining angels, demons and miracles in program specifications
• ZRC -- A refinement calculus for \(Z\)
• A tactic calculus. --- Abridged version
• A Weakest Precondition Semantics for Z
• Mathematics of Program Construction
• Integrated Formal Methods
• Theory and Applications of Relational Structures as Knowledge Instruments
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item