Angelic nondeterminism in the unifying theories of programming

DOI10.1007/s00165-006-0001-8zbMath1105.68012OpenAlexW2031356495MaRDI 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

relationssemanticsrefinementpredicate transformers

Mathematics Subject Classification ID

General topics in the theory of software (68N01)

Related Items

Taming Multirelations ⋮ Multirelations with infinite computations ⋮ Unifying theories in ProofPower-Z ⋮ Mechanised support for sound refinement tactics ⋮ Modelling higher-order dual nondeterminacy ⋮ An algebraic approach to multirelations and their properties ⋮ Angelic processes for CSP via the UTP ⋮ Angelicism in the Theory of Reactive Processes ⋮ Simulink Timed Models for Program Verification

Uses Software

• ZRC
• Circus

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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