Last active
August 29, 2015 14:01
-
-
Save nkavanagh/bc0f718a34e70bee6387 to your computer and use it in GitHub Desktop.
Dafny code to verify a Fibonacci implementation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| function method fibn(n: int, f1: int, f2: int): int | |
| requires n >= 0; | |
| decreases n; | |
| { | |
| if n > 1 then fibn(n-1, f2, f1+f2) else f2 | |
| } | |
| function method fib(n: int): int | |
| requires n >= 0; | |
| decreases n; | |
| { | |
| if n == 0 then n else fibn(n, 0, 1) | |
| } | |
| method testFib() | |
| { | |
| assert 0 == fib(0); | |
| assert 1 == fib(1); | |
| assert 2 == fib(3); | |
| assert 3 == fib(4); | |
| assert 55 == fib(10); | |
| assert 987 == fib(16); | |
| } | |
| method ifib(n: int) returns (f2: int) ensures f2 == fib(n); | |
| { | |
| var i: int := 0; | |
| var f1: int := 0; | |
| f2 := 0; | |
| while (i < n) | |
| invariant 0 <= i <= n; | |
| { | |
| f1 := f2; | |
| f2 := f1+f2; | |
| i := i + 1; | |
| } | |
| } |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
ifib is in-progress