5.4 Example

The following simple example illustrates an architectural specification definition (referencing ordinary specifications named List, Char, and Nat, assumed to declare the sorts Elem and List[Elem], Char, and Nat, respectively):

arch spec

CN_List =

units

 
C : Char ;
N : Nat ;
F : Elem -> List[Elem]

result

F[C fit Elem ^_|-> Char] and F[N fit Elem ^_|-> Nat]