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
|
// RUN: %dafny /dprint:- /env:0 /noVerify "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// 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;
{
}
// modifiers on functions
class CF {
static function F(): int
predicate method G()
copredicate Co()
protected function H(): int
static protected function method I(): real
protected static predicate method J()
}
// test printing of various if statements, including with omitted guards
module A {
method P(x: int, y: int) {
if x==2 {
} else if * {
}
if x==10 {
}
if y==0 {
} else if y==1 {
} else if * {
} else if y==2 {
} else if (*) {
} else if y == 3 {
} else {
}
}
}
module B refines A {
method P... {
if ... {
} else if x==3 {
}
...;
}
}
|
