(** {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 ghost ref q : int 
val ref r : int

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


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