Consistency and Semantics of Equational Definitions over Predefined Algebras

Abstract

We introduce and study the notion of an equational definition over a predefined algebra (EDPA) which is a modification of the notion of an algebraic specification enrichment. We argue that the latter is not quite appropriate when dealing with partial functions (in particular, with those defined by non-terminating functional programs), and suggest EDPA as a more adequate tool for specification and verification purposes. Several results concerning consistency of enrichments and correctness of EDPA are presented. The relations between EDPA and some other approaches to algebraic specification of partial functions are discussed.