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

(** {2 Integer square root} *)

use int.Int

function sqr (n:int) : int = n * n

val ref n : int
val ref count : int
val ref sum : int

let isqrt ()
  requires { n >= 0 }
  ensures  { count >= 0 }
  ensures  { sqr count <= n < sqr (count + 1) }
  diverges (** we are not yet attempting to prove termination *)
  =
  count <- 0; sum <- 1;
  while sum <= n do
    count <- count + 1;
    sum <- sum + 2 * count + 1
  done

let test ()
  diverges
  =
  n <- 42; isqrt(); count