blob: ae1a7d89a509ca128806756d904c399e01ec370a (
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
|
class Test {
var f1: int;
var f2: int;
predicate valid {
acc(f1) && acc(f2) && f1 == f2
}
method test()
requires valid
{
unfold valid
f1 := 2
f2 := 2
fold valid
/* --- not strictly necessary */
unfold valid
assert f1 == 2
fold valid
/* --- */
call test2()
unfold valid
assert f1 == 2 // BUG: this should not verify (1)
assert false // BUG: this should not verify (2)
}
method test2()
requires valid
ensures valid
ensures unfolding valid in f1 == 1 // line (1) above verifies also without this postcondition
{
unfold valid
f1 := 1
f2 := 1
fold valid
}
}
|
