blob: e9fef946be31ad97e644226e0fe716a13ab1eb87 (
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
|
module A {
method M(p: int) returns (y: int)
requires p <= 30;
{
assume p < 100;
var x;
assume x == p + 20;
x := x + 1;
while (*)
invariant x <= 120;
decreases 120 - x;
{
if (x == 120) { break; }
x := x + 1;
}
y := x;
}
}
module B refines A {
method M ...
{
assert p < 50;
assert ...;
var x := p + 20;
assert ...;
var k := x + 1;
...;
while ...
invariant k == x;
{
k := k + 1;
}
assert k == x || k == x + 1; // there are two exits from the loop
}
}
module C0 refines B {
method M ...
ensures y == 120; // error: this holds only if the loop does not end early
{
}
}
module C1 refines B {
method M ...
ensures y <= 120;
{
}
}
module C2 refines B {
method M ...
ensures y == 120;
{
...;
while (true)
...
assert k == x + 1; // only one loop exit remains
...;
}
}
|
