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

(** {2 Remainder of Euclidean division} *)

use int.Int

val ref x : int
val ref y : int
(* val ref q : int *)
val ref r : int

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


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