diff options
Diffstat (limited to 'Chalice/tests/regressions/workitem-10200.chalice')
| -rw-r--r-- | Chalice/tests/regressions/workitem-10200.chalice | 25 |
1 files changed, 0 insertions, 25 deletions
diff --git a/Chalice/tests/regressions/workitem-10200.chalice b/Chalice/tests/regressions/workitem-10200.chalice deleted file mode 100644 index a7394793..00000000 --- a/Chalice/tests/regressions/workitem-10200.chalice +++ /dev/null @@ -1,25 +0,0 @@ -class Test { - var f: int; - - function fib(n: int): int - requires n >= 0 - { - n < 2 ? n : fib(n - 1) + fib(n - 2) // incompletness: termination not atomatically proven - } - - method fibSeq(n: int) returns (r: int) - requires n >= 0 - requires acc(this.f) - ensures acc(this.f) - ensures r == fib(n) // previous error: the postcondition might not hold - { - if (n < 2) { - r := n - } else { - var f1: int; var f2: int - call f1 := fibSeq(n - 1) - call f2 := fibSeq(n - 2) - r := f1 + f2 - } - } -}
\ No newline at end of file |