Towards imperative modules: reasoning about invariants and sharing of mutable state
From MaRDI portal
Publication:854171
DOI10.1016/j.tcs.2006.07.035zbMath1118.68088OpenAlexW2043207621MaRDI QIDQ854171
Mike Barnett, David A. Naumann
Publication date: 7 December 2006
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2006.07.035
Related Items (3)
On assertion-based encapsulation for object invariants and simulations ⋮ Resources, concurrency, and local reasoning ⋮ Observational purity and encapsulation
Uses Software
Cites Work
- Soundness of data refinement for a higher-order imperative language
- How the design of JML accommodates both runtime assertion checking and formal verification
- A proof outline logic for object-oriented programming
- Ownership types for object encapsulation
- Separation and information hiding
- Ownership confinement ensures representation independence for object-oriented programs
- Stack-based access control and secure information flow
- Representation independence, confinement and access control [extended abstract]
- Separation logic and abstraction
- Computer Science Logic
- Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages
- Mathematics of Program Construction
- Programming Languages and Systems
- Theorem Proving in Higher Order Logics
- FM 2005: Formal Methods
- FM 2005: Formal Methods
- Formal Methods for Components and Objects
- Modular specification and verification of object-oriented programs
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Towards imperative modules: reasoning about invariants and sharing of mutable state
