A Trace model for pointers and objects

Object-oriented programs are notoriously prone to the following kinds of error, which could lead to increasingly severe problems in the presence of tasking: (1) following a null pointer; (2) deletion of an accessible object; (3) failure to delete an inaccessible object; (4) interference due to equality of pointers; (5) inhibition of optimisation due to fear of (4). Type disciplines and object classes are a great help in avoiding these errors. Stronger protection may be obtainable with the help of assertions, particularly invariants, which are intended to be true before and after each call of a method that updates the structure of the heap. This paper introduces a mathematical model and language for the formulation of assertions about objects and pointers, and suggests that a graphical calculus (Curtis & Lowe, 1995) may help in reasoning about program correctness. It deals with both garbage-collected heaps and the other kind. The theory is based on a trace model of graphs, using ideas from process algebra; and our development seeks to exploit this analogy as a unifying principle.