diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-02-16 13:55:58 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-02-16 13:55:58 -0800 |
| commit | e27219dff3dcf9f0307ebcb81fa8f94cf6156e7b (patch) | |
| tree | 3b6a6df7445cd20ae10378995df8b79861cb7914 /Test/dafny0/NoTypeArgs.dfy | |
| parent | 63786d11a607d337a71082d5b7555d791793d0f9 (diff) | |
Dafny: allow various forms of leaving off type arguments in declarations
Diffstat (limited to 'Test/dafny0/NoTypeArgs.dfy')
| -rw-r--r-- | Test/dafny0/NoTypeArgs.dfy | 82 |
1 files changed, 82 insertions, 0 deletions
diff --git a/Test/dafny0/NoTypeArgs.dfy b/Test/dafny0/NoTypeArgs.dfy new file mode 100644 index 00000000..c41c7990 --- /dev/null +++ b/Test/dafny0/NoTypeArgs.dfy @@ -0,0 +1,82 @@ +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);
+ }
+}
|