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
|
// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// -------- This is an example of what was once logically (although not trigger-ly) unsound ---
datatype Wrapper<T> = Wrap(T);
datatype Unit = It;
datatype Color = Yellow | Blue;
function F(a: Wrapper<Unit>): bool
ensures a == Wrapper.Wrap(Unit.It);
{
match a
case Wrap(u) => G(u)
}
function G(u: Unit): bool
ensures u == Unit.It;
{
match u
case It => true
}
method BadLemma(c0: Color, c1: Color)
ensures c0 == c1;
{
var w0 := Wrapper.Wrap(c0);
var w1 := Wrapper.Wrap(c1);
// Manually, add the following assertions in Boogie. (These would
// b93e ill-typed in Dafny.)
// assert _default.F($Heap, this, w#06);
// assert _default.F($Heap, this, w#17);
assert w0 == w1; // this would be bad news (it should be reported as an error)
}
method Main() {
BadLemma(Color.Yellow, Color.Blue);
assert false; // this shows how things can really go wrong if BadLemma verified successfully
}
// ---------------
class MyClass {
var x: int;
// The function axiom has "DType(this) == class.MyClass" in its antecedent. Hence, it
// is possible to prove the various asserts below only if the receiver is known by the
// verifier to be of type MyClass.
function H(): int { 5 }
}
datatype List = Nil | Cons(MyClass, List);
method M(list: List, S: set<MyClass>) returns (ret: int)
modifies S;
ensures ret == 7;
{ // error: postcondition violation (this postcondition tests that control does flow to the end)
match (list) {
case Nil =>
case Cons(r,tail) =>
if (r != null) {
ghost var h := r.H();
assert h == 5;
} else {
assert false; // error
}
}
var k := N();
assert k.H() == 5;
var st := new State;
ghost var l := st.NF();
assert l != null ==> l.H() == 5;
forall s | s in S ensures true; { assert s == null || s.H() == 5; }
forall s | s != null && s in S {
s.x := 0;
}
assert (forall t: MyClass :: t == null || t.H() == 5);
// note, the definedness problem in the next line sits inside an unreachable branch
assert (forall t: MyClass :: t != null ==> (if t.H() == 5 then true else 10 / 0 == 3));
assert TakesADatatype(List.Nil) == 12;
assert TakesADatatype(List.Cons(null, List.Nil)) == 12;
assert AlsoTakesADatatype(GenData.Pair(false, true)) == 17;
}
method N() returns (k: MyClass)
ensures k != null;
{
k := new MyClass;
}
class State {
var a: MyClass;
function NF(): MyClass reads this; { a }
}
function TakesADatatype(a: List): int { 12 }
datatype GenData<T> = Pair(T, T);
function AlsoTakesADatatype<U>(p: GenData<U>): int { 17 }
|
