diff options
| author |  rustanleino <unknown> | 2009-11-14 03:00:02 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2009-11-14 03:00:02 +0000 |
| commit | 2dfa38c856adff66a90a07a58171092af7f9186f (patch) | |
| tree | 76677462fc54de36aaf7407e06d82eb926f20cf4 /Test/dafny0/Datatypes.dfy | |
| parent | 17efb869d2b4a00c26e04b27de34b8bc643ad581 (diff) | |
Swapped previous file (Datatypes.bpl) for the correct test file (Datatypes.dfy).
Diffstat (limited to 'Test/dafny0/Datatypes.dfy')
| -rw-r--r-- | Test/dafny0/Datatypes.dfy | 63 |
1 files changed, 63 insertions, 0 deletions
diff --git a/Test/dafny0/Datatypes.dfy b/Test/dafny0/Datatypes.dfy new file mode 100644 index 00000000..4f247c79 --- /dev/null +++ b/Test/dafny0/Datatypes.dfy @@ -0,0 +1,63 @@ +datatype List<T> {
+ Nil;
+ Cons(T, List<T>);
+}
+
+class Node {
+ var data: int;
+ var next: Node;
+
+ function Repr(list: List<int>)
+ reads this;
+ { match list
+ case Nil =>
+ next == null
+ case Cons(d,cdr) =>
+ data == d && next.Repr(cdr)
+ }
+
+ method Init()
+ modifies this;
+ ensures Repr(this, #List<int>.Nil);
+ {
+ next := null;
+ }
+
+ method Add(d: int, L: List<int>) returns (r: Node)
+ requires Repr(L);
+ ensures r.Repr(#List<int>.Cons(d, L));
+ {
+ r := new Node;
+ r.data := d;
+ r.next := this;
+ }
+}
+
+class AnotherNode {
+ var data: int;
+ var next: AnotherNode;
+
+ function Repr(n: AnotherNode, list: List<int>)
+ reads n;
+ { match list
+ case Nil =>
+ n == null
+ case Cons(d,cdr) =>
+ n != null && n.data == d && Repr(n.next, cdr)
+ }
+
+ method Create() returns (n: AnotherNode)
+ ensures Repr(n, #List<int>.Nil);
+ {
+ n := null;
+ }
+
+ method Add(n: AnotherNode, d: int, L: List<int>) returns (r: AnotherNode)
+ requires Repr(n, L);
+ ensures Repr(r, #List<int>.Cons(d, L));
+ {
+ r := new AnotherNode;
+ r.data := d;
+ r.next := n;
+ }
+}
|