Proving Pointer Program Properties
Part 1: Context and overview
Bertrand Meyer, ETH Zürich, Switzerland


COLUMN
PDF Version

Abstract
Efforts to reason formally about programs, and in particular to prove their properties mathematically, have no practical value unless they can handle all the language facilities on which realistic programs depend. It is then not surprising that one of the biggest obstacles to the spread of such correctnessguaranteeing methods has been the lack of a good way to model the highly dynamic nature of the runtime structures created by objectoriented programs — and by most plain C or Pascal programs — with their heavy use of pointers, or references, from object to object.
The present discussion proposes a mathematical theory for modeling pointerrich object structures and proving their properties.
The model only uses simple concepts from set theory: sets, relations, functions, composition, restriction, image. For runtime operations all it needs is the notion of event, a function yielding a new program state from an existing one.
The model has two principal applications:
 The coarsegrained version of the model, considering only the existence or not of a reference between an object and another, gives a basis for discussing overall properties of the object structure, defining as a result the correctness constraints of memory management and especially garbage collection, full or incremental. Mathematically, this model uses a binary relation.
 The finegrained version, based on functions which together make up the relation of the coarsegrained version, integrates the properties of individual object fields. As a result, it allows proving the correctness of classes describing structures with luxurious pointer foliage, from linked lists and graphs to Btrees and doubleended queues.
This is part of a series of 3 articles. Parts 2 and 3 will be published in the MayJune 2003 issue of JOT.
Note: Due to the typographical sophistication of this column, no HTML version is available. Please use the PDF version.
About the author


Bertrand Meyer is Professor of Software Engineering at ETH Zürich and scientific advisor of ISE (Santa Barbara).

Cite this column as follows: Bertrand Meyer: “Proving Pointer Program Properties. Part 1: Context and overview”, in Journal of Object Technology, vol. 2, no. 2, MarchApril 2003, pp. 87108. http://www.jot.fm/issues/issue_2003_03/column8.
