diff options
| author |  Jason Koenig <unknown> | 2011-07-14 19:04:48 -0700 |
|---|---|---|
| committer | Jason Koenig <unknown> | 2011-07-14 19:04:48 -0700 |
| commit | 0ae617f31503b6723f76bf8036df373a1c7d91a6 (patch) | |
| tree | e88e90a9fafd7f2ceddff030fea764c8b50a5467 /Test/dafny0/Termination.dfy | |
| parent | c7b5aae8238f91da3efc9c7b558429b995f425c5 (diff) | |
Fixed failing regression tests.
Diffstat (limited to 'Test/dafny0/Termination.dfy')
| -rw-r--r-- | Test/dafny0/Termination.dfy | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy index f31935af..1482dc24 100644 --- a/Test/dafny0/Termination.dfy +++ b/Test/dafny0/Termination.dfy @@ -90,6 +90,11 @@ class Termination { method Traverse<T>(a: List<T>) returns (val: T, b: List<T>)
requires a != List.Nil;
ensures a == List.Cons(val, b);
+ {
+ match a {
+ case Cons(v, r) => val := v; b := r;
+ }
+ }
}
datatype List<T> = Nil | Cons(T, List<T>);
|