2 SORT-ITEM : Some Examples for DATATYPE-DECL

spec

LIST[sort Elem] =

sort

 

List[Elem] ::=

empty | sort Elem |
__ __:Elem×List[Elem]

...

end

An equivalent (and more verbose) specification for LIST[sort Elem] is the following:

spec

LIST[sort Elem] =

sort

List[Elem];
Elem<List[Elem]

ops

empty: -> List[Elem];
__ __:Elem×List[Elem] -> List[Elem]

...

end

It is often quite practical to provide selectors (as the_name_of and the_content_of in the FILE example) to easily recover the various parts from which a data is build.

spec

FILE =

sort

 

File ::= <__.__>:

(the_name_of__:Name) ×
(the_content_of__:Content)

end

An equivalent (and quite more verbose) specification for FILE is the following:

spec

FILE =

sort

File

ops

<__.__>: Name ×Content -> File;
the_name_of__: File -> Name;
the_content_of__:File -> Content

axioms

forall n:Name,  c:Content

.

the_name_of <n.c> = n

.

the_content_of <n.c> = c

end