blob: f7b6e07fb95273507c5fafbe588d5ee80000b81a (
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
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
124
125
126
127
128
129
130
131
132
133
134
|
module A {
class C {
var x: int;
predicate P()
reads this;
{
x < 100
}
method M()
modifies this;
ensures P();
{
x := 28;
}
method N()
modifies this;
ensures P();
{
x := -28;
}
}
}
module B refines A {
class C {
predicate P()
{
0 <= x
}
}
}
// ------------------------------------------------
module Loose {
class MyNumber {
var N: int;
ghost var Repr: set<object>;
predicate Valid
reads this, Repr;
{
this in Repr && null !in Repr &&
0 <= N
}
constructor Init()
modifies this;
ensures Valid && fresh(Repr - {this});
{
N, Repr := 0, {this};
}
method Inc()
requires Valid;
modifies Repr;
ensures old(N) < N;
ensures Valid && fresh(Repr - old(Repr));
{
N := N + 2;
}
method Get() returns (n: int)
requires Valid;
ensures n == N;
{
n := N;
}
}
}
module Tight refines Loose {
class MyNumber {
predicate Valid
{
N % 2 == 0
}
constructor Init()
ensures N == 0;
method Inc()
ensures N == old(N) + 2;
}
}
module UnawareClient imports Loose {
method Main() {
var n := new MyNumber.Init();
assert n.N == 0; // error: this is not known
n.Inc();
n.Inc();
var k := n.Get();
assert k == 4; // error: this is not known
}
}
module AwareClient imports Tight {
method Main() {
var n := new MyNumber.Init();
assert n.N == 0;
n.Inc();
n.Inc();
var k := n.Get();
assert k == 4;
}
}
// -------- Tricky refinement inheritance ----------------------------------------
module Tricky_Base {
class Tree {
var x: int;
predicate Constrained
reads this;
{
x < 10
}
predicate Valid
reads this;
{
x < 100
}
method Init()
modifies this;
ensures Valid;
{
x := 20;
}
}
}
module Tricky_Full refines Tricky_Base {
class Tree {
predicate Valid
{
Constrained // this causes an error to be generated for the inherited Init
}
}
}
|
