blob: 98e97cdbeffe78b565a2ff9524903faba58041a1 (
plain)
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
|
// RUN: %boogie "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// ------ the good ------
procedure F(x: int, y: int) returns (z: bool)
requires x < y;
ensures z == (x < 3);
{
start:
z := |{ var a : bool, b : bool; B: a := x < 3; return a; }|;
return;
}
function r(int): bool;
procedure F'(x: int, y: int) returns (z: bool)
{
start:
assume x < y;
assume (forall t: int :: x < 3 + t ==> r(t));
assert r(y);
}
procedure F''(x: int, y: int) returns (z: bool)
{
start:
assume x < y;
assume (forall t: int :: |{ var a: bool;
Start:
a := x < 3 + t;
goto X, Y;
X: assume a; return r(t);
Y: assume !a; return true;
}|);
assert r(y);
}
// ------ the bad ------
procedure G(x: int, y: int) returns (z: bool)
requires x < y;
ensures z == (x < 3);
{
start:
z := |{ var a : bool, b : bool; B: a := x < 3; return !a; }|;
return; // error: postcondition violation
}
procedure G'(x: int, y: int) returns (z: bool)
{
start:
assume x < y;
assume (forall t: int :: x + 3 < t ==> r(t));
assert r(y); // error
}
procedure G''(x: int, y: int) returns (z: bool)
{
start:
assume x < y;
assume (forall t: int :: |{ var a: bool;
Start:
a := x + 3 < t;
goto X, Y;
X: assume a; return r(t);
Y: assume !a; return true;
}|);
assert r(y); // error
}
|
