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
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
|
module A {
class C {
var x: int;
predicate Valid()
reads this;
{
0 <= x
}
function Get(): int
reads this;
{
x
}
constructor ()
modifies this;
ensures Valid();
{
x := 8;
}
method M()
requires Valid();
{
assert Get() == x;
assert x == 8; // error
}
}
}
module A' refines A {
class C {
predicate Valid...
{
x == 8
}
method N()
requires Valid();
{
assert Get() == x;
assert x == 8;
}
}
}
module B {
import X as A
method Main() {
var c := new X.C();
c.M(); // fine
c.x := c.x + 1;
c.M(); // error, because Valid() is opaque
}
method L(c: X.C)
requires c != null;
modifies c;
{
assert c.Get() == c.x; // error because Get() s opaque
if * {
assert c.Valid(); // error, because Valid() is opaque
} else if * {
c.x := 7;
assert c.Valid(); // error, because Valid() is opaque
} else {
c.x := 8;
assert c.Valid(); // error, because Valid() is opaque
}
}
}
module B_direct {
import X as A'
method Main() {
var c := new X.C();
c.M(); // fine
c.x := c.x + 1;
if * {
assert c.Valid(); // error, because Valid() is opaque
} else {
c.M(); // error, because Valid() is opaque
}
}
method L(c: X.C)
requires c != null;
modifies c;
{
assert c.Get() == c.x; // error because Get() s opaque
if * {
assert c.Valid(); // error, because Valid() is opaque
} else if * {
c.x := 7;
assert c.Valid(); // error, because Valid() is opaque
} else {
c.x := 8;
assert c.Valid(); // error, because Valid() is opaque
}
}
}
module B' refines B {
import X = A' // this by itself produces no more error
method Main'() {
var c := new X.C();
c.M(); // fine
c.x := c.x + 1;
if * {
assert c.Valid(); // error, because Valid() is opaque
} else {
c.M(); // error, because Valid() is opaque
}
}
method L'(c: X.C)
requires c != null;
modifies c;
{
assert c.Get() == c.x; // error because Get() s opaque
if * {
assert c.Valid(); // error, because Valid() is opaque
} else if * {
c.x := 7;
assert c.Valid(); // error, because Valid() is opaque
} else {
c.x := 8;
assert c.Valid(); // error, because Valid() is opaque
}
}
}
|
