Towards imperative modules: Reasoning about invariants and sharing of mutable state

David A. Naumann, Mike Barnett

Research output: Contribution to journalArticlepeer-review

17 Scopus citations

Abstract

Imperative and object-oriented programs make ubiquitous use of shared mutable objects. Updating a shared object can and often does transgress a boundary that was supposed to be established using static constructs such as a class with private fields. This paper shows how auxiliary fields can be used to express two state-dependent encapsulation disciplines: ownership, a kind of separation, and friendship, a kind of sharing. A methodology is given for specification and modular verification of encapsulated object invariants and shown sound for a class-based language. As an example the methodology is used to specify iterators, which are problematic for previous ownership systems.

Original languageEnglish
Pages (from-to)143-168
Number of pages26
JournalTheoretical Computer Science
Volume365
Issue number1-2
DOIs
StatePublished - 10 Nov 2006

Keywords

  • Alias control
  • Data abstraction
  • Object invariants
  • Program verification

Fingerprint

Dive into the research topics of 'Towards imperative modules: Reasoning about invariants and sharing of mutable state'. Together they form a unique fingerprint.

Cite this