Prev Up
Go backward to E.3.4 Add_Num_Efficiently
Go up to E.3 Architectural Specifications

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.


CoFI Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.
Comments to cofi-language@brics.dk

Prev Up