(** {1 MPRI lecture 2-36-1 "Proof of Programs"} *)

(** {2 Incrementing an array of reals *)

use int.Int
use real.RealInfix
use array.Array

(* increments by 1 all values between indices `i` (included) and `j` (excluded) *)
let incr_all (a:array real) (i j:int) : unit
  requires { 0 <= i <= j <= a.length }
  writes   { a }
  ensures { forall k:int. i <= k < j -> (old a[k]) +. 1.0 = a[k] }
  (* optional
     ensures  { forall k. 0 <= k < i -> a[k] = (old a[k]) }
     ensures  { forall k. j <= k < a.length -> a[k] = (old a[k]) }
  *)
 = for l = i to j-1 do
      invariant { forall k. i <= k < l -> a[k] = (old a)[k] +. 1.0 }
      (* necessary *)
      invariant { forall k:int. l <= k < j -> (old a[k]) = a[k] }
      (* optional
      invariant { forall k. 0 <= k < i -> a[k] = (old a[k]) }
      invariant { forall k. l <= k < a.length -> a[k] = (old a[k]) }
      *)
      a[l] <- a[l] +. 1.0
   done