Verification of programs operating on structured data

Abstract

The major method for verifying the correctness of computer programs is the inductive assertion approach. This approach has been limited in the past by the lack of techniques for handling data structures. In particular, there has been a need for concepts with which to describe structured data during intermediate and final stages of a computation. This thesis describes an approach by which this problem can be handled, and demonstrates its use in proving several programs correct. The key to the approach is the restriction of a data structure to a particular structural class. Primitive concepts are introduced which allow such a class to be concisely defined. Other concepts relate structures from a given class to data abstractions which the structures can be thought to represent. It is shown how to integrate the structural descriptions with the actual proofs of correctness by incorporating results of general applicability into a logical formalism for a given structural class.