summaryrefslogtreecommitdiff
path: root/Test/dafny0/NoTypeArgs.dfy
blob: 88418de7a35f5769051e328152c9ab03bbcf0451 (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
datatype List<T> = Nil | Cons(hd: T, tl: List);

method M0() {
  var l: List;
  l := Cons(5, Nil);
  assert l.hd == 5;

  var k: MyClass<bool>;
  k := new MyClass;
  k.data := false;

  var h := new MyClass;
  h.data := false;

  var y := new MyClass.Init(120);
  var z: int := y.data;
}

method M1() {  // same thing as above, but with types filled in explicitly
  var l: List<int>;
  l := Cons(5, Nil);
  assert l.hd == 5;

  var k: MyClass<bool>;
  k := new MyClass<bool>;
  k.data := false;

  var h := new MyClass<bool>;
  h.data := false;

  var y := new MyClass<int>.Init(120);
  var z: int := y.data;
}

class MyClass<G> {
  var data: G;
  method Init(g: G)
    modifies this;
  {
    data := g;
  }
}

// ---------------------------------------------------

// The followinng functions and methods are oblivious of the fact that
// List takes a type parameter.

function concat(xs: List, ys: List): List
{
  match xs
  case Nil => ys
  case Cons(x, tail) => Cons(x, concat(tail, ys))
}

function reverse(xs: List): List
{
  match xs
  case Nil => Nil
  case Cons(t, rest) => concat(reverse(rest), Cons(t, Nil))
}

ghost method Theorem(xs: List)
  ensures reverse(reverse(xs)) == xs;
{
  match (xs) {
    case Nil =>
    case Cons(t, rest) =>
      Lemma(reverse(rest), Cons(t, Nil));
  }
}

ghost method Lemma(xs: List, ys: List)
  ensures reverse(concat(xs, ys)) == concat(reverse(ys), reverse(xs));
{
  match (xs) {
    case Nil =>
      assert forall ws :: concat(ws, Nil) == ws;
    case Cons(t, rest) =>
      assert forall a, b, c :: concat(a, concat(b, c)) == concat(concat(a, b), c);
  }
}

// ------ Here are some test cases where the inferred arguments will be a prefix of the given ones

method DoAPrefix<A, B, C>(xs: List) returns (ys: List<A>)
{
  ys := xs;
}

function FDoAPrefix<A, B, C>(xs: List): List<A>
{
  xs
}