Friends Need a Bit More: Maintaining Invariants over Shared State

Mike Barnett, David A. Naumann

Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review

74 Scopus citations

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.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
EditorsDexter Kozen
Pages54-84
Number of pages31
DOIs
StatePublished - 2004

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3125
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Dive into the research topics of 'Friends Need a Bit More: Maintaining Invariants over Shared State'. Together they form a unique fingerprint.

Cite this