ZRC -- A refinement calculus for Z

DOI10.1007/S001650050016zbMATH Open0934.68062OpenAlexW2098243945MaRDI QIDQ1293891FDOQ1293891

Jim Woodcock, Ana Cavalcanti

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

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

zbMATH Keywords

specification language\(Z\) specifications

Mathematics Subject Classification ID

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

Cited In (18)

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

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)