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

(** {2 Naive Euclidean division} *)

use int.Int

val ref x : int
val ref y : int
val ref q : int
val ref r : int

let euclidean_div ()
  requires { x >= 0 }
  ensures { x = q * y + r /\ 0 <= r < y }
  diverges (** we are not yet attempting to prove termination *)
  =
   q <- 0; r <- x;
   while r >= y do
      invariant { x = q * y + r }
      invariant { 0 <= r }
      r <- r - y; q <- q + 1
   done

let test ()
  diverges (** we are not yet attempting to prove termination *)
  =
  x <- 42; y <- 17; euclidean_div(); (q,r)



(*
Local Variables:
compile-command: "why3 ide imp_euclidean_div_sol.mlw"
End:
*)