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
|
// RUN: %boogie "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// This file contains two definitions of integer div/mod (truncated division, as is
// used in C, C#, Java, and several other languages, and Euclidean division, which
// has mathematical appeal and is used by SMT Lib) and proves the correct
// correspondence between the two.
//
// Rustan Leino, 23 Sep 2010
function abs(x: int): int { if 0 <= x then x else -x }
function divt(int, int): int;
function modt(int, int): int;
axiom (forall a,b: int :: divt(a,b)*b + modt(a,b) == a);
axiom (forall a,b: int ::
(0 <= a ==> 0 <= modt(a,b) && modt(a,b) < abs(b)) &&
(a < 0 ==> -abs(b) < modt(a,b) && modt(a,b) <= 0));
function dive(int, int): int;
function mode(int, int): int;
axiom (forall a,b: int :: dive(a,b)*b + mode(a,b) == a);
axiom (forall a,b: int :: 0 <= mode(a,b) && mode(a,b) < abs(b));
procedure T_from_E(a,b: int) returns (q,r: int)
requires b != 0;
// It would be nice to prove:
// ensures q == divt(a,b);
// ensures r == modt(a,b);
// but since we know that the axioms about divt/modt have unique solutions (for
// non-zero b), we just prove that the axioms hold.
ensures q*b + r == a;
ensures 0 <= a ==> 0 <= r && r < abs(b);
ensures a < 0 ==> -abs(b) < r && r <= 0;
{
// note, this implementation uses only dive/mode
var qq,rr: int;
qq := dive(a,b);
rr := mode(a,b);
q := if 0 <= a || rr == 0 then qq else if 0 <= b then qq+1 else qq-1;
r := if 0 <= a || rr == 0 then rr else if 0 <= b then rr-b else rr+b;
assume {:captureState "end of T_from_E"} true;
}
procedure E_from_T(a,b: int) returns (q,r: int)
requires b != 0;
// It would be nice to prove:
// ensures q == dive(a,b);
// ensures r == mode(a,b);
// but since we know that the axioms about dive/mode have unique solutions (for
// non-zero b), we just prove that the axioms hold.
ensures q*b + r == a;
ensures 0 <= r;
ensures r < abs(b);
{
// note, this implementation uses only divt/modt
var qq,rr: int;
qq := divt(a,b);
rr := modt(a,b);
q := if 0 <= rr then qq else if 0 < b then qq-1 else qq+1;
r := if 0 <= rr then rr else if 0 < b then rr+b else rr-b;
}
|
