On assertion-based encapsulation for object invariants and simulations
From MaRDI portal
Publication:2643129
DOI10.1007/s00165-006-0020-5zbMath1123.68022OpenAlexW1989010503MaRDI QIDQ2643129
Publication date: 23 August 2007
Published in: Formal Aspects of Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00165-006-0020-5
Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Theory of software (68N99)
Related Items (1)
Uses Software
Cites Work
- Towards imperative modules: reasoning about invariants and sharing of mutable state
- Soundness of data refinement for a higher-order imperative language
- How the design of JML accommodates both runtime assertion checking and formal verification
- Tractable constraints in finite semilattices
- Program logic and equivalence in the presence of garbage collection.
- Algebraic reasoning for object-oriented programming
- Forward and backward simulations. I. Untimed Systems
- Proof of correctness of data representations
- 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
- Parametricity and local variables
- Parametric polymorphism and operational equivalence
- Data Refinement
- Representation independence, confinement and access control [extended abstract]
- Separation logic and abstraction
- Permission accounting in separation logic
- Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages
- Mathematics of Program Construction
- Fundamental Approaches to Software Engineering
- Programming Languages and Systems
- Programming Languages and Systems
- FM 2005: Formal Methods
- FM 2005: Formal Methods
- Modular specification and verification of object-oriented programs
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: On assertion-based encapsulation for object invariants and simulations