summaryrefslogtreecommitdiff
path: root/Test/dafny0/TypeAntecedents.dfy
blob: b6ef0d68d3f1f990e0655cf01c9f924d1ce2e519 (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
// -------- 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
  // be 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;
  ghost var l := NF();
  assert l != null ==> l.H() == 5;

  parallel (s | s in S) ensures true; { assert s == null || s.H() == 5; }
  parallel (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;
}
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 }