summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar Rustan Leino <unknown>2014-01-03 18:16:07 -0800
committerGravatar Rustan Leino <unknown>2014-01-03 18:16:07 -0800
commit5049ea124fe4b34f5c8fcb244663f3b68053643e (patch)
treeb0be1e8c391a8bbb0db8336e3c4c311010db060d /Test
parent4f86193513fa07374bc8295b875a0879b207621a (diff)
Renamed a constructor in a test file
Diffstat (limited to 'Test')
-rw-r--r--Test/dafny2/TreeFill.dfy10
1 files changed, 5 insertions, 5 deletions
diff --git a/Test/dafny2/TreeFill.dfy b/Test/dafny2/TreeFill.dfy
index f7e2cc89..3328aca9 100644
--- a/Test/dafny2/TreeFill.dfy
+++ b/Test/dafny2/TreeFill.dfy
@@ -1,9 +1,9 @@
-datatype Tree<T> = Null | Node(Tree, T, Tree);
+datatype Tree<T> = Leaf | Node(Tree, T, Tree)
function Contains<T>(t: Tree, v: T): bool
{
match t
- case Null => false
+ case Leaf => false
case Node(left, x, right) => x == v || Contains(left, v) || Contains(right, v)
}
@@ -14,12 +14,12 @@ method Fill<T>(t: Tree, a: array<T>, start: int) returns (end: int)
ensures forall i :: 0 <= i < start ==> a[i] == old(a[i]);
ensures forall i :: start <= i < end ==> Contains(t, a[i]);
{
- match (t) {
- case Null =>
+ match t {
+ case Leaf =>
end := start;
case Node(left, x, right) =>
end := Fill(left, a, start);
- if (end < a.Length) {
+ if end < a.Length {
a[end] := x;
end := Fill(right, a, end + 1);
}