Paper: Towards Imperative Modules: Reasoning about Invariants and Sharing of Mutable State (at LICS 2004)

Authors: David A. Naumann Michael Barnett

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.

BibTeX

  @InProceedings{NaumannBarnett-TowardsImperativeMo,
    author = 	 {David A. Naumann and Michael Barnett},
    title = 	 {Towards Imperative Modules: Reasoning about Invariants and Sharing of Mutable State},
    booktitle =  {Proceedings of the Nineteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2004)},
    year =	 {2004},
    month =	 {July}, 
    pages =      {313--323},
    location =   {Turku, Finland}, 
    publisher =	 {IEEE Computer Society Press}
  }