Abstract
In the context of a formal programming methodology and verification system for ownership-based invariants in object-oriented programs, a friendship system is defined. Friendship is a flexible protocol that allows invariants expressed over shared state. Such invariants are more expressive than those allowed in exisiting ownership type systems because they link objects that are not in the same ownership domain. Friendship permits the modular verification of cooperating classes. This paper defines friendship, sketches a soundness proof, and provides several realistic examples. © Springer-Verlag 2004.
Cite
CITATION STYLE
Barnett, M., & Naumann, D. A. (2004). Friends Need a Bit More: Maintaining Invariants over Shared State. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3125, 54–84. https://doi.org/10.1007/978-3-540-27764-4_5
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
