(** {1 MPRI lecture 2-36-1 "Proof of Programs"} *) (** {2 Inefficient sum} *) predicate _TO_BE_COMPLETED (* replace all occurrences of _TO_BE_COMPLETED below *) use int.Int val ref a : int val ref b : int val ref x : int val ref y : int let sum () requires { _TO_BE_COMPLETED } ensures { _TO_BE_COMPLETED } diverges (** we are not yet attempting to prove termination *) = x <- a; y <- b; while y > 0 do invariant { _TO_BE_COMPLETED } x <- x + 1; y <- y - 1 done (* Local Variables: compile-command: "why3 ide imp_sum.mlw" End: *)