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
|
// Simple.dfy
class MyClass<T, U> {
var x: int
method M(s: bool, lotsaObjects: set<object>)
returns (t: object, u: set<int>, v: seq<MyClass<bool,U>>)
requires s
modifies this, lotsaObjects
ensures t == t
ensures old(null) != this
{
x := 12;
while x < 100
invariant x <= 100
{
x := x + 17;
if x % 20 == 3 {
x := this.x + 1;
} else {
this.x := x + 0;
}
t, u, v := M(true, lotsaObjects);
var to: MyClass<T,U>;
to, u, v := this.M(true, lotsaObjects);
to, u, v := to.M(true, lotsaObjects);
assert v[x] != null ==> null !in v[2 .. x][1..][5 := v[this.x]][..10];
}
}
function F(x: int, y: int, h: WildData, k: WildData): WildData
{
if x < 0 then
h
else if x == 0 then
if if h == k then true else false then
h
else if y == 0 then
k
else
h
else
k
}
}
datatype List<T> = Nil | Cons(T, List<T>)
datatype WildData = Something | JustAboutAnything(bool, myName: set<int>, int, WildData) | More(List<int>)
class C {
var w: WildData
var list: List<bool>
}
class CF {
static function F(): int
predicate method G()
copredicate Co(): bool
protected function H(): int
static protected function method I(): real
static protected predicate method J()
}
lemma M(x: int)
ensures x < 8
{
}
colemma M'(x': int)
ensures true
{
}
Dafny program verifier finished with 0 verified, 0 errors
|
