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:

arch spec

Efficient_Add_Num =

units

 
N:Add_Num_Efficiently;
M:{ op succ(n:Num):Num = n+1 } given N

result

 
M hide 1, __0,__1,__ ++ __

end

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