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 | bd0939ffe92812966dfe2aac15d28cc1e3c37b42 (patch) | |
| tree | ea5861dcf473be51b024b7fe178e820e8be18c9d /Test/dafny0/Termination.dfy | |
| parent | 5e9cfe9da36b5efda394c1bde3f5536f1a5308a0 (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>);
|