Functional programming languages and executable algebraic specification languages do have a number of features in common. A functional program consists essentially of a collection of equations which define various functions. Functions are not restricted to ``normal'' data types, they can take functions as inputs and return a function as a result. Therefore, loosely speaking, functional programs consist of a number of equations whose left- and right- hand sides can contain compositions (combinations) of functions. Similarly, the semantics of the operations of an abstract data type are expressed in terms of a collection of axioms or equations which involve compositions (applications) of two or more operations.
The similarity in style between algebraic specifications and functional languages is illustrated in Fig. 9.6 which is a Miranda 9.1 script (program) which implements the data type queue. In common with most modern programming languages, Miranda has facilities which support data types and one such feature is the so-called ``algebraic type''. Such types are characterised by a set of constructors (which are precisely the atomic constructor operations of algebraic specifications).
Referring to the Miranda script of Fig. 9.6, the statement
Add queue num
introduces the data type queue where, following BNF notation, the symbol
::= means ``comprises'' and the symbol
denotes alternate
constructors. (In Miranda, constructors must start with an upper
case letter). The constructor Add takes two parameters, a queue and
a number.
The following three statements state the signature of the three operations remove, front and isempty while the six function definitions provide the semantics of the data type queue and correspond to the axioms of our algebraic specification. Note that Miranda employs postfix notation. Any conditions placed on the definition of a function (known as guards in Miranda) appear on the far right following the comma and the reserved word if. These guards must be predicate expressions which can be interpreted as either True or False.
For the queue q1 defined by
q1 = Add (Add (Add New 3) 4) 5
the applications
This similarity in style between executable algebraic specification languages and declarative or functional programming languages explains, in part, why such languages (for example, Miranda and SML) provide natural vehicles for rapid prototyping. In rapid prototyping the aim is to develop a trial model of a system quickly which exhibits all the important features of the intended system, but without the expenditure of excessive resources. Such prototyping provides a means for the production of a correct, although often inefficient implementation. This feature was introduced in chapter 7 and will be developed further in chapter 13 where we discuss prototyping algebraic specifications.
Often, however, at the end of the day, implementations are required which use some target high-level procedural language. In this case proofs that the implementation meets the specification should be carried out using the semantics of that target language. The onus on the implementor of the data type is to prove that every axiom and theorem of the algebraic specification is satisfied by the corresponding implementation. In practice, it usually suffices to prove that the axioms for each operation are satisfied by that operation's implementation. This proof obligation of verifying that an implementation satisfies its corresponding algebraic specification is an area of study that has still not been satisfactorily addressed in computer science. We will look briefly at some of the issues involved with respect to proof obligations for algebraic specifications later in chapter 12.
Exercise 9.7
Implement the algebraic specifications Binary-tree and Ordered-tree (Fig. 9.4 and Fig. 9.5 respectively) in Miranda.
