Prev Up Next
Go backward to E.3.3 Add_Num
Go up to E.3 Architectural Specifications
Go forward to E.3.5 Efficient_Add_Num

E.3.4 Add_Num_Efficiently

spec
Add_Num_Efficiently =
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

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

Prev Up Next