blob: 2583ef192feb7e7d9d508cb2bb06cbfd4961d2b9 (
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
|
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 {
class Client {
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 {
class Client {
method Main() {
var n := new MyNumber.Init();
assert n.N == 0;
n.Inc();
n.Inc();
var k := n.Get();
assert k == 4;
}
}
}
|
