-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathCtr_Ref_Boogie.bpl
51 lines (45 loc) · 1.62 KB
/
Ctr_Ref_Boogie.bpl
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
var ctrImpl:int; //State of the implementation
var ctrSpec:int; //State of the specification
//This method shows that refinement relation is preserved for the inc method
//Assume (sigma, inc(), sigma') is a valid step of the implementation
//We show that (refMap(sigma), inc(), refMap(sigma')) is a valid step of the specification as well
//refMap(sigma) == sigma (i.e., it is the identity function)
procedure refInc()
requires ctrImpl == ctrSpec;
modifies ctrImpl, ctrSpec;
ensures ctrImpl == ctrSpec;
{
//inc ctrImpl
ctrImpl := ctrImpl + 1;
//inc ctrSpec
ctrSpec := ctrSpec + 1;
}
//This method shows that refinement relation is preserved for the dec method
//Assume (sigma, dec(), sigma') is a valid step of the implementation
//We show that (refMap(sigma), dec(), refMap(sigma')) is a valid step of the specification as well
//refMap(sigma) == sigma (i.e., it is the identity function)
procedure refDec()
requires ctrImpl == ctrSpec;
modifies ctrImpl, ctrSpec;
ensures ctrImpl == ctrSpec;
{
//dec ctrImpl
ctrImpl := ctrImpl - 1;
//dec ctrSpec
ctrSpec := ctrSpec - 1;
}
//This method shows that refinement relation is preserved for the read method
//Assume (sigma, read()=>c, sigma') is a valid step of the implementation
//We show that (refMap(sigma), read()=>c, refMap(sigma')) is a valid step of the specification as well
//refMap(sigma) == sigma (i.e., it is the identity function)
procedure refRead()
requires ctrImpl == ctrSpec;
ensures ctrImpl == ctrSpec;
{
var r1:int, r2:int;
//read ctrImpl
r1 := ctrImpl;
//dec ctrSpec
r2 := ctrSpec;
assert r1 == r2;
}