blob: f93a1eeb540a19ec50fbffee2d2535b37bab76a2 (
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
|
class FoldUnfoldExperiments
{
var x:int;
var y:int;
var z:int;
var w:int;
predicate X { acc(x) }
predicate Y { acc(y) }
predicate Z { acc(z) }
function getX():int
requires X;
{ unfolding X in x }
function getY():int
requires Y;
{ unfolding Y in y }
function getZ():int
requires Z;
{ unfolding Z in z }
method setX(v:int)
requires X;
ensures X && getX()==v;
{
unfold X; x:=v; fold X;
}
// this method checks if the methodology frames correctly around a method call: what happens with folded data and unfolded data
// also: what happens if we have folded data during the call, that we unfold after the call
method check()
requires acc(x) && acc(y) && acc(z) && acc(w);
ensures acc(y) && y==2 && X && getX()==3 && Z && getZ()==4 && acc(w) && w==10;
{
x:=1; y:=2; z:=4; w:=10;
fold X; fold Y; fold Z;
call setX(3);
unfold Y;
}
// this method checks that method calls do not interfere with the correct handling of folds and unfolds
method check1()
requires X && acc(y) && y==1;
ensures acc(y) && y==1 && X && getX()==200;
{
call setX(10);
fold Y;
call setX(100);
unfold Y;
fold Y;
unfold Y;
call setX(200);
}
}
|
