blob: 55fe8ff554342e00c7d62f55863c798d5b3fc455 (
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
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
|
// 4 errors expected
class C {
method M(x: int) returns (y: bool)
requires 0 <= x;
ensures y <==> x == 10;
{
y := true;
if (x != 10) { y := !y; }
}
method Caller0()
{
var b: bool;
call b := M(12);
assert !b;
call b := M(10);
assert b;
}
method Caller1()
{
var b: bool;
call b := M(11);
assert b; // error (258)
}
var F: int;
method P(n: int)
requires acc(F);
ensures F == old(F) + n; // error
{
F := F + n;
}
method Caller2()
requires acc(F);
{
var prev := F;
call P(2);
assert false; // succeeds because postcondition of P is not well-defined (i.e. we do not havoc this.F, so the verifier assumes the value is the same in pre and post)
}
method Q(n: int)
requires acc(F);
ensures acc(F) && F == old(F) + n;
{
F := F + n;
}
method Caller3()
requires acc(F);
ensures acc(F);
{
var prev := F;
call Q(2);
assert F == prev + 2;
}
}
class Consts {
method M0() returns (z: int)
ensures z == 5
{
const a := 5
z := a
}
method M1() {
ghost const a
a := 5
}
method M2() {
ghost const a
a := 5
a := 5 // error (569)
}
method M3(b: bool) {
ghost const a
if (b) { a := 5 }
assert a < 10 // error (611)
}
method M4(b: bool) {
ghost const a
if (b) { a := 5 }
ghost var x := a
if (!b) { a := 7 }
assert a < 10
assert b ==> x == 5 // cool, huh?
}
method M5(b: bool) {
ghost const a
if (b) { a := 5 }
assert assigned(a) ==> a == 5
}
}
|
