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
|
// My first Dafny program
// Rustan Leino, 27 January 2008
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
}
}
// some datatype stuff:
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>;
}
lemma M(x: int)
ensures x < 8;
{
// proof would go here
}
colemma M'(x': int)
ensures true;
{
}
|
