4.4 Example

The following example illustrates a complete structured specification definition (referencing a specification named Partial_Order, which is assumed to declare the sort Elem and the predicate __ < __):

spec

List_with_Order [Partial_Order] =

free type

List[Elem] ::= nil | cons(hd:?Elem; tl:?List[Elem])

then

 

local

 

op

insert : Elem × List[Elem] -> List[Elem];

vars

x,y : Elem; l : List[Elem]

axioms

insert(x,nil) = cons(x,nil);

x < y => insert(x,cons(y,l)) = cons(x,insert(y,l));

¬ (x < y) => insert(x,cons(y,l)) = cons(y,insert(x,l))

within

 

pred

order[__ < __] : List[Elem] × List[Elem]

vars

x : Elem; l : List[Elem]

axioms

order[__ < __](nil) = nil;

order[__ < __](cons(x,l)) = insert(x,order[__ < __](l))

end