Setting up algebraic specifications
Loe M. G. Feijs, Hans B. M. Jonkers · Cambridge University Press eBooks · 1992
Introduction This chapter is about setting up flat algebraic specifications. This involves the introduction of more COLD-K constructs and the formulation of various methodological guidelines. At the end of the previous chapter we had to conclude that we almost succeeded in specifying the natural numbers, the only problem being that the expressive power to express the minimality of Nat was lacking. This expressive power will be available after we have introduced the inductive predicate definitions below. We shall complete the example of the natural numbers and we shall investigate various technical aspects of inductive definitions – which unfortunately are quite non-trivial. In addition to inductive predicate definitions, we shall also have inductive function definitions. We address issues like ‘proof obligations’ for inductive definitions, consistency and completeness. Finally we give a number of complete examples of flat algebraic specifications: queues, stacks, bags and symbolic expressions. Inductive predicate definitions An inductive predicate definition defines a predicate as the least predicate satisfying some assertion (provided that this predicate exists). Before turning our attention to the syntactic machinery available in COLD-K for expressing this, we ought to explain this notion of ‘least’. Therefore we shall formulate what we mean by one predicate being ‘less than or equal to’ another predicate. Definition . A predicate r is less than or equal to a predicate q if for each argument x we have that r ( x ) implies q ( x ). We illustrate this definition by means of two unary predicates p1 and p2. We assume the sort Nat with its operations zero and succ as specified before.