(** {1 MPRI lecture 2-36-1 "Proof of Programs"} *) (** {2 Naive Euclidean division, with local variables} *) use int.Int let euclidean_div (x y:int) : (int,int) requires { x >= 0 } ensures { let (q,r) = result in x = q * y + r /\ 0 <= r < y } diverges (** we are not yet attempting to prove termination *) = let ref q = 0 in let ref r = x in while r >= y do invariant { x = q * y + r } invariant { 0 <= r } r <- r - y; q <- q + 1 done; (q,r) let test (a b: int) requires { a >= 0 } diverges (** we are not yet attempting to prove termination *) = let (q,r) = euclidean_div a b in (q,r,q*b+r) (* run test for example using: why3 execute euclidean_div_with_locals.mlw --use Top "test 42 17" *) (* Local Variables: compile-command: "why3 ide euclidean_div_with_locals.mlw" End: *)