E.3.5 Efficient_Add_Num

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

unit spec

Implement_Succ_by_Plus =

 

Num_Monoid ->

{ Num_Monoid then  op succ(n:Num):Num=n+1 }

end

arch spec

Efficient_Add_Num =

units

 
F:Implement_Succ_by_Plus;
N:Add_Num_Efficiently

result

 
F[N hide __0,__1,__ ++ __ ] hide 1

end

%% We have now that Efficient_Add_Num is a refinement of Add_Num.