Wiki Agenda Contact Version française

An example from EWD 673

An example from Dijkstra's paper EWD 673: On weak and strong termination


Authors: Jean-Christophe Filliâtre

Topics: Tricky termination

Tools: Why3

see also the index (by topic, by tool, by reference, by year)


(* EWD 673: On Weak and Strong Termination *)

module EWD673

  use import bool.Bool
  use import int.Int
  use import int.Lex2
  use import 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