Building Specifications in the Event-B Institution

DOI10.46298/lmcs-18(4:4)2022OpenAlexW3138937708MaRDI QIDQ5060190

Marie Farrell, James F. Power, Rosemary Monahan

Publication date: 9 January 2023

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2103.10881v6

zbMATH Keywords

formal semanticsinstitutionsrefinementEvent-Bmodularisation

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Related Items

Building Specifications in the Event-B Institution

Uses Software

• Dafny
• CASL
• Haskell
• Hets
• Rodin
• Circus

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A theoretical basis for stepwise refinement and the programming calculus
• Foundations of algebraic specification and formal software development.
• The behavioural semantics of Event-B refinement
• Categorical foundations for structured specifications in \(\mathsf{Z}\)
• A UTP semantics for \textsf{Circus}
• Specifications in an arbitrary institution
• CASL reference manual. The complete documentation of the common algebraic specification language.
• Dafny: An Automatic Program Verifier for Functional Correctness
• On the Purpose of Event-B Proof Obligations
• The Composition of Event-B Models
• Institutions: abstract model theory for specification and programming
• Refinement Calculus
• Building Specifications in the Event-B Institution
• An Institution for Event-B
• General Refinement, Part One: Interfaces, Determinism and Special Refinement
• General Refinement, Part Two: Flexible Refinement
• An axiomatic basis for computer programming