mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
f91bb58b89
Description: - Choice was made to not add unused variables when there is no contract and no body (no pre/(x)post, and no body). - For postcondition variable result, we only check variables that are not of unit type. And, we report a warning only if the variable is not present in all the ensures. - For result variable, with several imbricated raise, it seems possible to have false positive with no location. Removing the no location case which seems unhelpful anyway
34 lines
614 B
Plaintext
34 lines
614 B
Plaintext
module M
|
|
|
|
use int.Int
|
|
use ref.Ref
|
|
|
|
(** 1. A loop increasing [i] up to 10. *)
|
|
|
|
val i : ref int
|
|
|
|
let loop1 (_u:unit) requires { !i <= 10 } ensures { !i = 10 }
|
|
= while !i < 10 do
|
|
invariant { !i <= 10 } variant { 10 - !i }
|
|
i := !i + 1
|
|
done
|
|
|
|
|
|
(** 2. The same loop, followed by a function call. *)
|
|
|
|
val x: ref int
|
|
|
|
let negate (_u:unit) ensures { !x = - (old !x) } = x := - !x
|
|
|
|
let loop2 (_u:unit) requires { !x <= 10 }
|
|
= begin
|
|
while !x < 10 do invariant { !x <= 10 } variant { 10 - !x }
|
|
x := !x + 1
|
|
done;
|
|
assert { !x = 10 };
|
|
if !x > 0 then (negate ());
|
|
assert { !x = -10 }
|
|
end
|
|
|
|
end
|