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

  nist_ge_n (n-1);

  nist_ge_n (n-2)
  end

test: this can be proved by instantiating the previous lemma

goal test : nist 42 >= 17