A PROLOG environment for developing and reasoning about data types

Abstract

PROLOG is a programming language based on first order logic. The feature that distinguishes PROLOG from most other programming languages is that the execution of PROLOG programs is based on subgoal reduction and unification. Unfortunately, the reliance on unification for execution has also inhibited PROLOG from utilizing some recently developed concepts in programming languages such as abstract data types. In this paper we introduce a discipline for incorporating abstract data types into PROLOG, and study the use of PROLOG as a uniform programming environment for the specification, implementation, and verification of PROLOG programs. We illustrate the application of the environment to the development of abstract data types in PROLOG. In addition to producing executable specifications, the proposed discipline also provides automatic means of refining a specification into an implementation. We also present a PROLOG-based inductive theorem proving method for proving properties of data types and correctness of implementations.