1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
|
//@+ CheckArithOverflow = no
/*@ lemma real_add_int :
@ (\forall integer x y; (real) (x + y) == (real) x + (real) y);
@*/
/*@ lemma real_mul_int :
@ (\forall integer x y; (real) (x * y) == (real) x * (real) y);
@*/
/*@ lemma mul_add_distr1 :
@ (\forall real x y z; x * (y + z) == (x * y) + (x * z));
@*/
/*@ lemma add_comm :
@ (\forall real x y; x + y == y + x);
@*/
/*@ lemma add_assoc :
@ (\forall real x y z; x + (y + z) == (x + y) + z);
@*/
/* @ lemma PRECISION_property :
@ 0.01 * (real) DecimalAbstractReal.PRECISION == 1.0;
@*/
/* @ lemma PRECISION_property :
@ 0.01 * (real) 100 == 1.0;
@*/
/*@ lemma PRECISION_property_real :
@ 0.01 * 100.0 == 1.0;
@*/
/*@ logic real amount_real_value{L}(DecimalAbstractReal x) {
@ (real) x.intPart + 0.01 * (real) x.decPart }
@*/
/*@ logic integer amount_cent_value{L}(DecimalAbstractReal x) {
@ DecimalAbstractReal.PRECISION * x.intPart + x.decPart
@ }
@*/
public class DecimalAbstractReal {
/** minimal fraction of currency = 1/PRECISION */
public static final short PRECISION = 100;
short intPart;
short decPart;
//@ invariant decimal: 0 <= decPart && decPart < 100;
// bug: should be PRECISION ;
/*@ requires a != null;
@ assigns intPart, decPart;
@ behavior real_value:
@ ensures
@ amount_real_value(this) ==
@ \old(amount_real_value(this)) + \old(amount_real_value(a));
@ behavior cent_value:
@ ensures
@ amount_cent_value(this) ==
@ \old(amount_cent_value(this)) + \old(amount_cent_value(a));
@
@*/
public void add(DecimalAbstractReal a) {
short d = (short)(decPart + a.decPart);
short i = (short)(intPart + a.intPart);
if (d >= PRECISION) {
d -= PRECISION;
i++;
}
intPart = i;
decPart = d;
}
/*@ requires a != null && a != this;
@ assigns intPart, decPart;
@ behavior real_value:
@ ensures
@ amount_real_value(this) ==
@ \old(amount_real_value(this)) + amount_real_value(a);
@ behavior cent_value:
@ ensures
@ amount_cent_value(this) ==
@ \old(amount_cent_value(this)) + amount_cent_value(a);
@
@*/
public void add2(DecimalAbstractReal a) {
short d = (short)(decPart + a.decPart);
short i = (short)(intPart + a.intPart);
if (d >= PRECISION) {
d -= PRECISION;
i++;
}
intPart = i;
decPart = d;
}
}
|
