Friends need a bit more: Maintaining invariants over shared state

DOI10.1007/978-3-540-27764-4_5MaRDI QIDQ5313101zbMATH OpenOpenAlexFDO

Authors Mike Barnett, David A. Naumann

Publication date 26 August 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b98756

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Towards imperative modules: reasoning about invariants and sharing of mutable state
• Modular verification of static class invariants
• Formal Methods for Components and Objects
• Modular invariants for layered object structures
• Controlling object allocation using creation guards

Cited in

(12)

• A system for compositional verification of asynchronous objects
• Verified software units
• A proof outline logic for object-oriented programming
• On assertion-based encapsulation for object invariants and simulations
• Specification and verification challenges for sequential object-oriented programs
• From predicates to programs: the semantics of a method language
• Invariants for non-hierarchical object structures
• The dynamic frames theory
• A Representation-Independent Behavioral Semantics for Object-Oriented Components
• The concept of class invariant in object-oriented programming
• Towards imperative modules: reasoning about invariants and sharing of mutable state
• Automatic verification of Java programs with dynamic frames

Describes a project that uses

Uses Software

• ESC/Java

This page was built for publication: Friends need a bit more: Maintaining invariants over shared state

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