blob: ad654308f34ffec8d969773de56ea90de8f6142d (
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
|
// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
class UnboundedStack<T> {
var top: Node<T>;
ghost var footprint: set<object>;
ghost var content: seq<T>;
function IsUnboundedStack(): bool
reads {this} + footprint;
{
this in footprint &&
(top == null ==> content == []) &&
(top != null ==> top in footprint && top.footprint <= footprint &&
top.prev == null && content == top.content && top.Valid())
}
function IsEmpty(): bool
reads {this};
{ content == [] }
method Pop() returns (result: T)
requires IsUnboundedStack() && !IsEmpty();
modifies footprint;
ensures IsUnboundedStack() && content == old(content)[1..];
{
result := top.val;
// The following assert does the trick, because it gets inlined and thus
// exposes top.next.Valid() (if top.next != null):
footprint := footprint - top.footprint; top := top.next;
// In a previous version of the implementation of the SplitExpr transformation, the
// following assert did not have the intended effect of being used as a lemma:
assert top != null ==> top.Valid();
if (top != null) {
footprint := footprint + top.footprint; top.prev := null;
}
content := content[1..];
} }
class Node<T> {
var val: T;
var next: Node<T>;
var prev: Node<T>;
var footprint: set<Node<T>>;
var content: seq<T>;
function Valid(): bool
reads this, footprint;
{
this in footprint && !(null in footprint) &&
(next == null ==> content == [val]) &&
(next != null ==> next in footprint &&
next.footprint < footprint &&
!(this in next.footprint) &&
next.prev == this &&
content == [val] + next.content &&
next.Valid())
}
}
// ---------------------------------------------------------------------------------------
// The following examples requires that quantifiers are boosted (that is, #2) when checked
// versus not boosted (#1) when assumed.
function F(x: nat): int
{
if x == 0 then 0 else 1 + F(x-1)
}
method M(N: nat)
{
var i := 0;
while (i < N)
invariant forall x {:induction false} :: 0 <= x <= i ==> F(x) == x;
{
i := i + 1;
}
}
// ----- orderings of checked vs. free -----
// The translation must always put checked things before free things. In most situations,
// this does not actually matter, but it does matter for loop invariants of loops that have
// no backedges (that is, loops where Boogie's simple dead-code analysis figures prunes
// away the backedges.
predicate AnyPredicate(a: int, b: int) { a <= b }
method NoLoop(N: nat)
{
var i;
while i < N
invariant AnyPredicate(i, N); // error: may not hold initially
{
i := i + 1;
break; // this makes the loop not a loop
}
assert AnyPredicate(i, N);
}
|
