Reasoning about object structures using ownership

Abstract

Many well-established concepts of object-oriented programming work for individual objects, but do not support object structures. The development of a verifying compiler requires enhancements of programming theory to cope with this deficiency. In this paper, we support this position by showing that classical specification and verification techniques support invariants for individual objects whose fields are primitive values, but are unsound for invariants involving more complex object structures. We have developed an ownership model, which allows one to structure the object store and to restrict reference passing and the operations that can be performed on references. We use this model to generalize classical object invariants to cover such object structures. We summarize the state of our work and identify open research challenges. © IFIP International Federation for Information Processing 2008.