On assertion-based encapsulation for object invariants and simulations

DOI10.1007/S00165-006-0020-5zbMath1123.68022OpenAlexW1989010503MaRDI QIDQ2643129

David A. Naumann

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

zbMATH Keywords

Encapsulation and abstractionObject invariantsSeparation and alias control

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Theory of software (68N99)

Related Items (1)

Blaming the client: on data refinement in the presence of pointers

Uses Software

• Eiffel
• Spec#

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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

This page was built for publication: On assertion-based encapsulation for object invariants and simulations