Example of an arch spec

[Till Mossakowski <till@informatik.uni-bremen.de>]

Dear Peter,

I have used the following example to explain the need of
architectural specifications. Perhaps it is also useful
for Appendix E.

spec Monoid =  ... see M-4

spec Num =  ... see M-4

spec AddNum =   ... see M-4

(It would make sense to rename the stuff from M-4 to become
compatible with the stuff in Appendix E. For example, both
Monoid specs should collapse into one and the same spec.
Num and Nat can be kept distinct, because they follow different
styles. But I assume that plus of Num is replaced with
__+__.)

spec AddNumEff =
  sort Num
  ops 0,1:Num
      __0, __1:Num -> Num
      __+__, __++__ : Num*Num -> Num
  vars x,y:Num
  axioms
    0 0=0               0 1=1
    x 0+y 0=(x+y) 0     x 0++y 0=(x+y) 1
    x 0+y 1=(x+y) 1     x 0++y 1=(x++y) 0
    x 1+y 0=(x+y) 1     x 1++y 0=(x++y) 0
    x 1+y 1=(x++y) 0    x 1++y 1=(x++y) 1
    %% __+__ is binary addition 
    %% __++__ is binary addition with carry
end

spec NatMon =
  Monoid with Thing |-> Num, null |-> 0, o |-> plus
end

unit spec Implement_Succ_by_Plus =
  NatMon -> NatMon then 
                   op succ:Num->Num
                   var n:Num
                   axiom succ(n)=n+1      
end

%% It is more efficient to implement successor in terms of
%% (binary) addition, while it is easier to specify
%% addition in terms of successor than as binary addition.
%% Thus, the structure of the implementation differs
%% from the structure of the specification:

arch spec Efficient_Add_Num =
  units
    F:Implement_Succ_by_Plus
    N:AddNumEff
  result
    F[N hide __0,__1,__++__] hide 1
    %% may also be written as F[N] hide 1 ???? Andrzej???
    %% (or at least F[N fit 0 |-> 0] hide 1)
end



Greetings,
Till