Initial set of files.

1 files changed, 74 insertions, 0 deletions

diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy
new file mode 100644
index 00000000..f6e0a2b4
--- /dev/null
+++ b/Test/dafny0/DTypes.dfy
@@ -0,0 +1,74 @@
+class C {

+  var n: set<Node>;

+

+  method M(v: Stack)

+    requires v != null;

+  {

+    var o: object := v;

+    assert !(o in n);  // should be known from the types involved

+  }

+

+  method N(v: Stack)

+    /* this time without the precondition */

+  {

+    var o: object := v;

+    assert !(o in n);  // error: v may be null

+  }

+

+  method A0(a: CP<int,C>, b: CP<int,object>)

+  {

+    var x: object := a;

+    var y: object := b;

+    assert x == y ==> x == null;

+  }

+

+  method A1(a: CP<int,C>)

+  {

+    var x: object := a;

+    assert (forall b: CP<int,Stack> :: x == b ==> b == null);  // error (we don't add a type antecedent to

+                                                               // quantifiers; is that what we want?)

+  }

+

+  var a2x: set<CP<C,Node>>;

+  method A2(b: set<CP<Node,C>>)

+    requires !(null in b);

+  {

+    var x: set<object> := a2x;

+    var y: set<object> := b;

+    assert x * y == {};

+  }

+

+  method A3(b: set<CP<Node,C>>)

+    /* this time without the precondition */

+  {

+    var x: set<object> := a2x;

+    var y: set<object> := b;

+    assert x * y <= {null};

+  }

+

+  method A4(b: set<CP<Node,C>>)

+    /* again, without the precondition */

+  {

+    var x: set<object> := a2x;

+    var y: set<object> := b;

+    assert x * y == {};  // error

+  }

+

+  method A5()

+  {

+    var a := new CP<int,C>;

+    var b := new CP<int,object>;

+    while (a != null) {

+      var x: object := a;

+      var y: object := b;

+      assert x == y ==> x == null;

+      a := a;  // make 'a' a loop target

+    }

+  }

+}

+

+class Stack { }

+class Node { }

+

+class CP<T,U> {

+}