On assertion-based encapsulation for object invariants and simulations

DOI10.1007/S00165-006-0020-5MaRDI QIDQ2643129zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Formal Methods for Components and Objects
• Towards imperative modules: reasoning about invariants and sharing of mutable state
• Modular Specification of Encapsulated Object-Oriented Components
• Specification and verification of encapsulation in Java programs
• FM 2005: Formal Methods

Cites work

• A proof outline logic for object-oriented programming
• Algebraic reasoning for object-oriented programming
• Data Refinement
• FM 2005: Formal Methods
• FM 2005: Formal Methods
• Forward and backward simulations. I. Untimed Systems
• Fundamental Approaches to Software Engineering
• How the design of JML accommodates both runtime assertion checking and formal verification
• scientific article; zbMATH DE number 1728235 (Why is no real title available?)
• scientific article; zbMATH DE number 4050933 (Why is no real title available?)
• scientific article; zbMATH DE number 3748394 (Why is no real title available?)
• scientific article; zbMATH DE number 1006119 (Why is no real title available?)
• scientific article; zbMATH DE number 1032897 (Why is no real title available?)
• scientific article; zbMATH DE number 1105469 (Why is no real title available?)
• scientific article; zbMATH DE number 1860624 (Why is no real title available?)
• scientific article; zbMATH DE number 2090153 (Why is no real title available?)
• Mathematics of Program Construction
• Modular specification and verification of object-oriented programs
• Ownership confinement ensures representation independence for object-oriented programs
• Ownership types for object encapsulation
• Parametric polymorphism and operational equivalence
• Parametricity and local variables
• Permission accounting in separation logic
• Program logic and equivalence in the presence of garbage collection.
• Programming Languages and Systems
• Programming Languages and Systems
• Proof of correctness of data representations
• Representation independence, confinement and access control (extended abstract)
• Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages
• Separation and information hiding
• Separation logic and abstraction
• Soundness of data refinement for a higher-order imperative language
• Towards imperative modules: reasoning about invariants and sharing of mutable state
• Tractable constraints in finite semilattices

Cited in

(6)

• scientific article; zbMATH DE number 1728234 (Why is no real title available?)
• Modular Specification of Encapsulated Object-Oriented Components
• Specification and verification of encapsulation in Java programs
• FM 2005: Formal Methods
• Formal Methods for Components and Objects
• Blaming the client: on data refinement in the presence of pointers

Describes a project that uses

Uses Software

• Eiffel
• Spec#

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2643129)