mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
23 lines
294 B
Plaintext
23 lines
294 B
Plaintext
module M
|
|
|
|
use int.Int
|
|
use ref.Ref
|
|
|
|
exception Break
|
|
|
|
let f (n : int) : int ensures { result <= 10 }
|
|
= let i = ref n in
|
|
try
|
|
while (!i > 0) do
|
|
invariant { true }
|
|
variant { !i }
|
|
if (!i <= 10) then raise Break;
|
|
i := !i - 1
|
|
done
|
|
with Break -> ()
|
|
end;
|
|
!i
|
|
|
|
end
|
|
|