Commit 968f8cfa by Jean-Christophe Filliâtre

### new fibonacci examples

parent 5c7e86d5
 ... ... @@ -43,6 +43,41 @@ module FibonacciLinear end module FibRecGhost "recursive version, using ghost code" use import Fibonacci use import int.Int let rec fib_aux (ghost n: int) (a b k: int) : int requires { 0 <= n && a = fib n && b = fib (n+1) } ensures { result = fib (n+k) } = if k = 0 then a else fib_aux (n+1) b (a+b) (k-1) let fib (n: int) : int requires { 0 <= n } ensures { result = fib n } = fib_aux 0 0 1 n end module FibRecNoGhost "recursive version, without ghost code" use import Fibonacci use import int.Int let rec fib_aux (a b k: int) : int requires { exists n: int. 0 <= n && a = fib n && b = fib (n+1) } ensures { forall n: int. 0 <= n && a = fib n && b = fib (n+1) -> result = fib (n+k) } = if k = 0 then a else fib_aux b (a+b) (k-1) let fib (n: int) : int requires { 0 <= n } ensures { result = fib n } = fib_aux 0 1 n end theory Mat22 "2x2 integer matrices" use import int.Int ... ...
 ... ... @@ -11,24 +11,36 @@ version="2.4.1"/>
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!