TY - CHAP
T1 - Friends Need a Bit More
T2 - Maintaining Invariants over Shared State
AU - Barnett, Mike
AU - Naumann, David A.
PY - 2004
Y1 - 2004
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=35048827919&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=35048827919&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-27764-4_5
DO - 10.1007/978-3-540-27764-4_5
M3 - Chapter
AN - SCOPUS:35048827919
SN - 3540223800
SN - 9783540223801
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 54
EP - 84
BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
A2 - Kozen, Dexter
ER -