Algorithmic Specifications: A Constructive Specification Method for Abstract Data Types

Abstract

This paper presents a new specification method for abstract data types and a pertaining logic. The specification method proposed differs from the classical algebraic one by its constructive, yet abstract nature. Although it leads to a different style in specification, the method avoids some fundamental problems inherent in the algebraic specification method. The logic proposed is essentially a first-order logic for strict (partial) functions. It allows in particular the expression of the semantic conditions guaranteeing the consistency of a specification.