Modular invariants for layered object structures

DOI10.1016/J.SCICO.2006.03.001zbMath1100.68539OpenAlexW2103591546MaRDI QIDQ2507783

Gary T. Leavens, Arnd Poetzsch-Heffter, Peter Müller

Publication date: 5 October 2006

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/20.500.11850/69749

zbMATH Keywords

invariantvisibilityobject-oriented programmingmodular verificationownershipJML

Mathematics Subject Classification ID

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

Related Items (11)

Holistic Specifications for Robust Programs ⋮ Specification and verification challenges for sequential object-oriented programs ⋮ Verification of mutable linear data structures and iterator-based algorithms in Dafny ⋮ Verification of object-oriented programs: a transformational approach ⋮ Verified software units ⋮ Verification of Concurrent Systems with VerCors ⋮ Universe Types for Topology and Encapsulation ⋮ Dynamic Frames in Java Dynamic Logic ⋮ Unifying separation logic and region logic to allow interoperability ⋮ An operational semantics for object-oriented concepts based on the class hierarchy ⋮ Invariants for Non-Hierarchical Object Structures

Uses Software

• Eiffel
• JML
• KeY
• Unnamed Item
• Unnamed Item

This page was built for publication: Modular invariants for layered object structures