(** {1 MPRI lecture 2-36-1 "Proof of Programs"} *) (** {2 McCarthy's ``91'' function} *) use int.Int let rec f91 (n:int) : int variant { 100 - n } ensures { result = if n <= 100 then 91 else n - 10 } = if n <= 100 then f91(f91 (n + 11)) else n - 10 (* Local Variables: compile-command: "why3 ide mccarthy_sol.mlw" End: *)