Wiki Agenda Contact Version française

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