mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
24 lines
468 B
Plaintext
24 lines
468 B
Plaintext
|
|
(* 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
|