diff options
author | 2009-11-20 23:04:27 +0000 | |
---|---|---|
committer | 2009-11-20 23:04:27 +0000 | |
commit | 9ed23deb0a3db4b61cf07fc6b551e10bc5436837 (patch) | |
tree | 23f152c4938c27ff110dae14c1f0bea039a9ae09 /Test/dafny0/Datatypes.dfy | |
parent | 797711ee7fb126a081e00d8b247c0cfa83ddd3f2 (diff) |
Added resolution and translation of algebraic datatypes and (in function bodies) match expressions.
Addressed a couple of todos, including checking the well-formedness of quantifiers and if-then-else expressions in function bodies.
Diffstat (limited to 'Test/dafny0/Datatypes.dfy')
-rw-r--r-- | Test/dafny0/Datatypes.dfy | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/Test/dafny0/Datatypes.dfy b/Test/dafny0/Datatypes.dfy index 4f247c79..61ae9cb6 100644 --- a/Test/dafny0/Datatypes.dfy +++ b/Test/dafny0/Datatypes.dfy @@ -7,25 +7,25 @@ class Node { var data: int;
var next: Node;
- function Repr(list: List<int>)
+ function Repr(list: List<int>): bool
reads this;
{ match list
case Nil =>
next == null
case Cons(d,cdr) =>
- data == d && next.Repr(cdr)
+ data == d && next != null && next.Repr(cdr)
}
method Init()
modifies this;
- ensures Repr(this, #List<int>.Nil);
+ ensures Repr(#List.Nil);
{
next := null;
}
method Add(d: int, L: List<int>) returns (r: Node)
requires Repr(L);
- ensures r.Repr(#List<int>.Cons(d, L));
+ ensures r.Repr(#List.Cons(d, L));
{
r := new Node;
r.data := d;
@@ -37,7 +37,7 @@ class AnotherNode { var data: int;
var next: AnotherNode;
- function Repr(n: AnotherNode, list: List<int>)
+ function Repr(n: AnotherNode, list: List<int>): bool
reads n;
{ match list
case Nil =>
@@ -47,14 +47,14 @@ class AnotherNode { }
method Create() returns (n: AnotherNode)
- ensures Repr(n, #List<int>.Nil);
+ ensures Repr(n, #List.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));
+ ensures Repr(r, #List.Cons(d, L));
{
r := new AnotherNode;
r.data := d;
|