Chair of Software Engineering

Proving Program Pointer Properties
Bertrand Meyer

Work In Progress

This series of four articles, currently in draft form, provides a general model for reasoning about the properties of run-time structures involving references (pointers) between objects.

The articles (all PDF) are the following:

Part 1: Context and overview.

Part 2: The overall object structure. (Revision: 20 March 2003.)

Part 3: Considering individual fields.

Part 4: Proving properties of data structure classes.

The last article is not yet available in the same form as the others parts, but the results so far are covered in a self-contained article written to be readable independently of the rest: Towards practical proofs of class correctness. (Revision: 17 February 2003)