This section provides examples that illustrate the CASL language constructs for use in architectural specifications: architectural specification definitions, unit declarations, unit definitions, unit specifications, and unit expressions.
A definition of an architectural specification specifies some units and how to compose them, e.g.:
A model of the above architectural specification consists of a unit N, a unit function F, and the unit F[N], which is itself a model of the structured specification List [Nat].
- arch spec
- Imp_Nat_List =
- units
N : Nat ; F : Nat -> List [Nat] - result
- F[N]
A unit declaration names a unit that is to be developed, and gives its type. When the type is an ordinary specification, the unit is to be an ordinary model of it; when the type is a function type, the unit is to be a function from (compatible) ordinary models to ordinary models that extend the arguments. Some examples of unit declarations:
The form of unit declaration using `given' provides an implicit declaration of a unit function that gets applied just once. If the declaration of F were to be replaced by that of L in the architectural specification example given above (letting the result be simply L as well) then an implementation of the architectural specification would still involve providing a function that could give an implementation of List [Nat] extending any implementation N of Nat.
- N : Nat
- L : List [Nat] given N
- F : Nat -> List [Nat]
A unit definition names a unit that can be obtained from previous units (in the same architectural specification), possibly involving fitting, hiding, translation, etc.:
A unit specification definition names a unit type, allowing it to be reused. E.g.:
A unit declaration may then refer to it, as in F : Gen_List.
- unit spec
- Gen_List = Nat -> List [Nat]
Architectural specifications themselves may also be used as unit specifications.
The various forms of unit expression mostly resemble those of structured specifications: