Go backward to Multiple parameters
Go up to More subtle points

Fixed part of a parameter specification

Let us consider again the STACK-OF-ELEM specification used as a starting point in Section 1, where we have explained how to identify ELEM as a parameter specification, leading to STACK(par ELEM).

An alternative to the solution proposed so far would have been to indicate in the body of the definition of STACK that ELEM was to be considered as a parameter, leading to the following specification: 

spec GENERIC-STACK = 
  enrich par ELEM by   % Note the ``par'' here !
    sort Stack
    opns ...here the usual signature of Stack, with some
         operations referring to the sort Elem in their profile,
         e.g. push: Stack Elem -> Stack , and some not, 
         e.g. empty: -> Stack ...
    axioms ...here the usual axioms...
endspec.
Very important note: This alternative is not adequate, since to know by which specifications a given specification SP is parametrized, it is necessary to inspect the body of the definition of the specification SP, and this recursively (i.e. it is also necessary to inspect the definitions of the named specifications referred to in the definition of SP, etc.). In a word, this alternative is totally disastrous w.r.t. our purposes. It is mentioned here for explanatory purposes only, and should be discarded as soon as the need for fixed parts in parameter specifications is understood.

Let us now consider a more complex example. Assume for instance that we want to describe a generic specification of stacks, where elements are equipped with some weight (which for some reason should be in the interval [0..10]). Let us start by giving the non generic version: 

spec STACK-OF-WEIGHTED-ELEM =
  enrich(
      enrich persistently NATURAL by
        sort Elem
        opns: Weight: Elem -> Nat
        axioms: 
          forall e:Elem. Weight(e) leq 10
  ) by
    sort Stack
    opns ...here the usual signature of Stack, with some
         operation using the weight of the elements...
    axioms ...here some axioms...
endspec.
Now let us turn the above STACK-OF-WEIGHTED-ELEM specification into a generic specification, using for explanatory purposes the alternative syntax described above: 
spec GENERIC-STACK-OF-WEIGHTED-ELEM =
  enrich(
      enrich persistently NATURAL by 
        par   % Note the ``par'' here !
          sort Elem
          opns: Weight: Elem -> Nat
          axioms: 
            forall e:Elem. Weight(e) leq 10
  ) by
    sort Stack
    opns ...here the usual signature of Stack, with some
         operation using the weight of the elements...
    axioms ...here some axioms...
endspec.
Note that here the keyword par ranges over the expected parameter part, i.e. over the persistent extension of NATURAL by sort Elem, opns: Weight etc. Now let us try to turn the specification STACK-OF-WEIGHTED-ELEM into a generic specification according to the proposal for generic specifications described in this note. For this we have to identify a parameter specification which should first of all be a correct specification. The chunk sort Elem, opns: Weight etc. is not convenient, since it does not define a true signature. Hence the only possibility is to define: 
spec WEIGHTED-ELEM =
  enrich persistently NATURAL by
    sort Elem
    opns: Weight: Elem -> Nat
    axioms: 
      forall e:Elem. Weight(e) leq 10
endspec.
and then stacks of weighted elements can be specified as follows: 
spec BAD-STACK-WEIGHT(par WEIGHTED-ELEM) =
    sort Stack
    opns ...here the usual signature of Stack, with some
         operation using the weight of the elements...
    axioms ...here some axioms...
endspec.
Unfortunately, NATURAL has been made part of the parameter specification, which was not exactly what was intended by the specifier. Indeed, when instantiating the parameter specification WEIGHTED-ELEM, it is not adequate (according to the specifier's intentions) to consider that all sorts, function and predicate symbols of the signature of WEIGHTED-ELEM are symbols to be instantiated. Only the sort Elem and the function symbol Weight are subject to actualization, while the signature of NATURAL is "fixed". In other words, in any instantiation of STACK-WEIGHT (i.e. actualization of WEIGHTED-ELEM by some argument specification SP), the specifier expects that the fitting morphism (from the signature of WEIGHTED-ELEM to the signature of SP) used to determine the actualization leaves the signature of NATURAL invariant.

Therefore, we suggest to introduce an additional construct that will allow the specifier to precisely describe in a parameter specification the part that is intended to be instantiated and the part that is "fixed". During instantiation, it is then easy to check that the fitting morphism provided is the identity on the "fixed" part. This leads to the following version of the specification of stacks of elements equipped with a weight: 

spec GOOD-STACK-WEIGHT(par WEIGHTED-ELEM fixing NATURAL) =
    sort Stack
    opns ...here the usual signature of Stack, with some
         operation using the weight of the elements...
    axioms ...here some axioms...
endspec.
According to this new construct, all well-formedness conditions given so far regarding disjointness of signatures are relaxed (it is not necessary to require disjointness w.r.t. the fixed signatures).
CoFI Study Notes, November 3, 1996

Prev Up