An example from EWD 673
An example from Dijkstra's paper EWD 673: On weak and strong termination
Auteurs: Jean-Christophe Filliâtre
Catégories: Tricky termination
Outils: Why3
see also the index (by topic, by tool, by reference, by year)
(* EWD 673: On Weak and Strong Termination *) module EWD673 use bool.Bool use int.Int use ref.Refint val any_bool () : bool val any_nat () : int ensures { result >= 0 } let s (x: ref int) (y: ref int) = requires { !x >= 0 /\ !y >= 0 } while !x > 0 || !y > 0 do invariant { !x >= 0 /\ !y >= 0 } variant { !x, !y } if !x > 0 then begin decr x; y := any_nat () end; (* else *) if !y > 0 then decr y done end
download ZIP archive