Friends need a bit more: Maintaining invariants over shared state. (English) Zbl 1106.68338

Kozen, Dexter (ed.), Mathematics of program construction. 7th international conference, MPC 2004, Stirling, Scotland, UK, July 12–14, 2004. Proceedings. Berlin: Springer (ISBN 3-540-22380-0/pbk). Lecture Notes in Computer Science 3125, 54-84 (2004).
Summary: 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.
For the entire collection see [Zbl 1053.68005].


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


Full Text: DOI