ZRC -- A refinement calculus for Z

DOI10.1007/S001650050016MaRDI QIDQ1293891zbMATH OpenOpenAlexFDO

Authors Ana Cavalcanti, Jim Woodcock

Publication date 29 June 1999

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

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

zbMATH Keywords

\(Z\) specificationsspecification language

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 2080003
• A Weakest Precondition Semantics for Z
• A logic for schema-based program development
• A calculus of refinements for program derivations
• scientific article; zbMATH DE number 605917

Cited in

(22)

• A UTP semantics for \textsf{Circus}
• Laws of mission-based programming
• Safety-critical Java programs from \textsf{Circus} models
• Refinement and the Z schema calculus
• scientific article; zbMATH DE number 4026807 (Why is no real title available?)
• A Weakest Precondition Semantics for Z
• Mechanised support for sound refinement tactics
• *ZFC: An axiomatic * approach to nonstandard methods
• scientific article; zbMATH DE number 2080003 (Why is no real title available?)
• scientific article; zbMATH DE number 1487939 (Why is no real title available?)
• A tactic language for refinement of state-rich concurrent specifications
• Transformation rules for Z
• ZB 2005: Formal Specification and Development in Z and B
• A formal software development approach using refinement calculus
• Imperative abstractions for functional actions
• From control law diagrams to Ada via \textsf{Circus}
• UTP, \textsf{\textit{Circus}}, and Isabelle
• Towards a model-checker for \textit{\textsf{Circus}}
• \textit{\textsf{Circus2CSP}}: a tool for model-checking \textit{\textsf{Circus}} using FDR
• ArcAngel: a tactic language for refinement
• Test-data generation for control coverage by proof
• Angelic nondeterminism in the unifying theories of programming

Describes a project that uses

Uses Software

• ZRC

This page was built for publication: ZRC -- A refinement calculus for \(Z\)

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