examples/ewd673.mlw

   1
   2 (* EWD 673: On Weak and Strong Termination *)
   3
   4 module EWD673
   5
   6   use bool.Bool
   7   use int.Int
   8   use ref.Refint
   9
  10   val any_bool () : bool
  11   val any_nat  () : int ensures { result >= 0 }
  12
  13   let s (x: ref int) (y: ref int) =
  14     requires { !x >= 0 /\ !y >= 0 }
  15     while !x > 0 || !y > 0 do
  16       invariant { !x >= 0 /\ !y >= 0 }
  17       variant   { !x, !y }
  18       if !x > 0 then begin decr x; y := any_nat () end;
  19       (* else *)
  20       if !y > 0 then decr y
  21     done
  22
  23 end