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
|
type C _;
function f<a>(C a) returns (int);
axiom (forall<a> x : C a :: f(x) == 42);
procedure P(a : C int) returns () {
start:
assert f(a) == 42;
assert f(a) == 43; // should not be provable
}
procedure Q<a>(c : C a) returns () {
start:
assert f(c) == 42;
assert f(c) == 43; // should not be provable
}
function g<a,b>(a, b) returns (int);
axiom (forall x : int, y : bool :: g(x,y) == 13);
axiom (forall<a> x : int, y : C a :: g(x,y) == 42);
axiom (forall<a,z> x : C z, y : C a :: g(x,y) == 43);
procedure R() returns () {
start:
assert g(7, true) == 13;
assert g(7, false) == 15; // should not be provable
}
procedure S<b>(y : C b) returns () {
start:
assert g(3, y) == f(y);
assert g(y, false) == 15; // should not be provable
}
procedure T<a,b>(y : C b, param : a) returns () {
var x : C a; var z : C b;
start:
assert g(y, x) == g(x, y);
assert g(y, x) == 43;
assert g(f(x), y) == 42;
assert g(y, z) == 15; // should not be provable
}
type D _ _;
procedure U() returns () {
var u : D int bool, v : D bool int;
start:
assume (forall<a,b> x:D a b, y:b :: g(x, y) == -3);
assert g(v, 32) == -3;
assert g(v, 716371398712982312321) == -3;
assert g(u, 1) == -3; // should not be provable
}
|
