Param specs/arch specs

[bkb@informatik.uni-bremen.de (Bernd Krieg-Brueckner)]

Till and I have tried to reconsider our view w.r.t. need for names for
algebras as formal parameters in architectural specifications etc. in the
light of the question: how much can be done with the small solution (as is,
i.e. *without* names for formal parameters) and what cannot be expressed /
can only be awkwardly expressed (from our point of view). The conclusion
is:
(a) we can live with the solution as is (although we would prefer the
"larger" solution now), provided
(b) names for algebras as formal parameters are introduced "smoothly" in an
extension which then also covers higher-order properly etc.

Indeed, much can be expressed in the "small" solution, but at the expense
of a lot of renaming.

Consider the specification of the implementation of pairs by arrays
of length two (and vice versa), i.e. informally: pair (x, x) as 
array [1..2] x, where it is important that the two instances of x in 
pair are the same x (i.e. the same algebra in the example).

First, we present it with using
specifications parameterized by algebras, explicit algebra parameter names,
and dot notation:


spec ELEM =
  sort elem
end spec

spec PAIR (X,Y:ELEM) =
  sort pair
  opns (_,_) : X.elem >< Y.elem -> pair
       selx : pair -> X.elem
       sely : pair -> Y.elem
  axioms forall x:X.elem, y:Y.elem . selx((x,y))=x
         forall x:X.elem, y:Y.elem . sely((x,y))=y
         forall p:pair . (selx(p),sely(p))=p
end spec

spec ARRAY (Index,Elem:ELEM) =
   sort array
   opns mt : array
        _[_]:=_ : array >< Index.elem >< Elem.elem -> array
        _[_] : array >< Index.elem -o-> Elem.elem
   axioms forall i:Index.elem . not (D(mt[i]))
          forall i:Index.elem, x:Elem.elem, a:array . [a[i]:=x]i = x
          ...
end spec

spec TWO = enrich ELEM by
  opns 1,2:elem
  axioms forall x:elem . (x=1 \/ x=2)
end spec

arc spec PAIR-AND-ARRAY =
  decl Two:TWO
  decl PairAsArray : X:ELEM >< A:ARRAY(Two,X) -> PAIR(X,X)
  decl ArrayAsPair : X:ELEM >< P:PAIR(X,X) ->  A:ARRAY(Two,X)
end spec


Now the use of explicit algebra parameter names and dot notation can
be avoided by (a somewhat cumbersome, but probably still manageable)
renaming:

spec ELEM =
  sort elem
end spec

spec ELEM1 = ELEM where elem --> elem1 end spec
spec ELEM2 = ELEM where elem --> elem2 end spec

spec PAIR [ELEM1,ELEM2] =
  sort pair
  opns (_,_) : elem1 >< elem2 -> pair
       selx : pair -> elem1
       sely : pair -> elem2
  axioms forall x:elem1, y:elem2 . selx((x,y))=x
         forall x:elem1, y:elem2 . sely((x,y))=y
         forall p:pair . (selx(p),sely(p))=p
end spec

spec INDEX = ELEM where elem --> index
end spec

spec ARRAY [INDEX,ELEM] =
   sort array
   opns mt : array
        _[_]:=_ : array >< index >< elem -> array
        _[_] : array >< index -o-> elem
   axioms forall i:index . not (D(mt[i]))
          forall i:index, x:elem, a:array . [a[i]:=x]i = x
          ...
end spec

spec TWO = enrich ELEM by
  opns 1,2:elem
  axioms forall x:elem . (x=1 \/ x=2)
end spec

arc spec PAIR-AND-ARRAY =
  decl Two:TWO
  decl PairAsArray : ELEM >< ARRAY[TWO for INDEX where index --> elem]
                     -> PAIR[ELEM for ELEM1 where elem1 --> elem,
                             ELEM for ELEM2 where elem2 --> elem]

  decl ArrayAsPair : ELEM >< PAIR[ELEM for ELEM1 where elem1 --> elem,
                                  ELEM for ELEM2 where elem2 --> elem]
                     -> ARRAY[TWO for INDEX where index --> elem]
end spec

But we cannot express the application of specifications parameterized
by algebras appropriately: The declared algbra Two:TWO cannot by fed
into ARRAY as above, but instead PairAsArray and ArrayAsPair are
parameterized by ARRAY[TWO for INDEX where index --> elem], a
specification which contains TWO, but cannot be (partially)
instantiated with Two.  More generally, without specifiations
parameterized by algebras, we cannot instantiate parameterized specs
with previously declared algebras, which is a loss of expressive
power.

___________________________________________________________________
Prof. Dr. Bernd Krieg-Brueckner    courier mail only:
FB3 Mathematik und Informatik      MZH 8071, FB3
Universitaet Bremen                Universitaet Bremen
Postfach 330 440                   Bibliothekstr. 1
D-28334 Bremen                     D-28359 Bremen

Telefon: (+49) 421-218-3660        telefax: (+49) 421-218-3054
bkb@Informatik.Uni-Bremen.DE       privat:  (+49) 421-25-1024
NEW: http://www.informatik.uni-bremen.de/~bkb