## 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