examples/nistonacci.mlw

   1
   2 (** {1 Nistonacci numbers}
   3
   4     The simple "Nistonacci numbers" example, originally designed by
   5     K. Rustan M. Leino for the SSAS workshop (Sound Static Analysis
   6     for Security, NIST, Gaithersburg, MD, USA, June 27-28, 2018) *)
   7
   8 use int.Int
   9
  10
  11 (** {2 Specification}
  12
  13     new in Why3 1.0: (pure) program function that goes into the logic
  14     (no need for axioms anymore to define such a function)
  15  *)
  16
  17 let rec ghost function nist(n:int) : int
  18   requires { n >= 0 }
  19   variant { n }
  20 = if n < 2 then n else nist (n-2) + 2 * nist (n-1)
  21
  22 (** {2 Implementation} *)
  23
  24 use ref.Ref
  25
  26 let rec nistonacci (n:int) : int
  27   requires { n >= 0 }
  28   variant { n }
  29   ensures { result = nist n }
  30 = let x = ref 0 in
  31   let y = ref 1 in
  32   for i=0 to n-1 do
  33     invariant { !x = nist i }
  34     invariant { !y = nist (i+1) }
  35      let tmp = !x in
  36      x := !y;
  37      y := tmp + 2 * !y
  38   done;
  39   !x
  40
  41 (** {2 A general lemma on Nistonacci numbers}
  42
  43   That lemma function is used to prove the lemma `forall n. nist(n) >=
  44     n` by induction on `n`
  45
  46 *)
  47
  48 (***  (new in Why3 1.0: markdown in comments !) *)
  49
  50 let rec lemma nist_ge_n (n:int)
  51    requires { n >= 0 }
  52    variant { n }
  53    ensures { nist(n) >= n }
  54 = if n >= 2 then begin
  55   (** recursive call on `n-1`, acts as using the induction
  56       hypothesis on `n-1` *)
  57   nist_ge_n (n-1);
  58   (** let's also use induction hypothesis on `n-2` *)
  59   nist_ge_n (n-2)
  60   end
  61
  62
  63 (** test: this can be proved by instantiating the previous lemma *)
  64
  65 goal test : nist 42 >= 17