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

David A. Naumann, Mike Barnett

Research output: Contribution to journalConference articlepeer-review

21 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 local co-dependence, 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.

Original languageEnglish
Pages (from-to)313-322
Number of pages10
JournalProceedings - Symposium on Logic in Computer Science
Volume19
DOIs
StatePublished - 2004
EventProceedings of the 19th Annual IEEE Symposium on Logic in Computer Science - Turku, Finland
Duration: 13 Jul 200417 Jul 2004

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