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