Pointers and data abstractions in high level languages—II: Correctness proofs

Recognizing the problems that the use of pointers pose to the construction of reliable software, this two-part paper proposes a scheme by which pointers may be used in a controlled manner to build data abstractions without being used as abstractions in their own right. Part I, published in Computer Languages 2, 135–148, presents the language constructs facilitating the proposal. Part II, in this Issue, attempts to show, by use of a fairly complex example, that proving the correctness of an implementation of an abstraction built in this manner from pointers need not be more difficult than other implementation correctness proofs.