A toy variant of Fibonacci function
A variant of Fibonacci, making a simple illustration of the so-called ``let functions'' and ``lemma functions''.
Authors: Claude Marché
Topics: Ghost code
Tools: Why3
see also the index (by topic, by tool, by reference, by year)
Nistonacci numbers
The simple "Nistonacci numbers" example, originally designed by K. Rustan M. Leino for the SSAS workshop (Sound Static Analysis for Security, NIST, Gaithersburg, MD, USA, June 27-28, 2018)
use int.Int
Specification
new in Why3 1.0: (pure) program function that goes into the logic (no need for axioms anymore to define such a function)
let rec ghost function nist(n:int) : int requires { n >= 0 } variant { n } = if n < 2 then n else nist (n-2) + 2 * nist (n-1)
Implementation
use ref.Ref let rec nistonacci (n:int) : int requires { n >= 0 } variant { n } ensures { result = nist n } = let x = ref 0 in let y = ref 1 in for i=0 to n-1 do invariant { !x = nist i } invariant { !y = nist (i+1) } let tmp = !x in x := !y; y := tmp + 2 * !y done; !x
A general lemma on Nistonacci numbers
That lemma function is used to prove the lemma forall n. nist(n) >=
n
by induction on n
let rec lemma nist_ge_n (n:int) requires { n >= 0 } variant { n } ensures { nist(n) >= n } = if n >= 2 then begin
recursive call on n-1
, acts as using the induction
hypothesis on n-1
nist_ge_n (n-1);
let's also use induction hypothesis on n-2
nist_ge_n (n-2) end
test: this can be proved by instantiating the previous lemma
goal test : nist 42 >= 17
download ZIP archive