ewd673.mlw 511 Bytes
Newer Older
1 2 3 4 5 6 7 8

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

module EWD673

  use import bool.Bool
  use import int.Int
  use import int.Lex2
9
  use import ref.Refint
10

11 12
  val any_bool () : bool
  val any_nat  () : int ensures { result >= 0 }
13 14

  let s (x: ref int) (y: ref int) =
15
    requires { !x >= 0 /\ !y >= 0 }
16 17
    while !x > 0 || !y > 0 do
      invariant { !x >= 0 /\ !y >= 0 }
18
      variant   { !x, !y }
19 20 21 22 23 24
      if !x > 0 then begin decr x; y := any_nat () end;
      (* else *)
      if !y > 0 then decr y
    done

end