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
45 lines
1.2 KiB
Plaintext
45 lines
1.2 KiB
Plaintext
module M
|
|
|
|
use int.Int
|
|
use ref.Ref
|
|
|
|
(** Recursive functions *)
|
|
|
|
(** 1. Pure function *)
|
|
|
|
let rec f1 (x:int) : int variant { x }
|
|
requires { x >= 0 } ensures { result = 0 }
|
|
= if x > 0 then (f1 (x-1)) else x
|
|
|
|
(** 2. With effects but no argument *)
|
|
|
|
val x : ref int
|
|
|
|
let rec f2 (_u:unit) : unit variant { !x }
|
|
requires { !x >= 0 } ensures { !x = 0 }
|
|
= if !x > 0 then begin x := !x - 1; f2 () end
|
|
|
|
(** 3. With effects and a pure argument *)
|
|
|
|
let rec f3 (a:int) : unit variant { a }
|
|
requires { a >= 0 } ensures { !x = old !x + a }
|
|
= if a > 0 then begin x := !x + 1; (f3 (a-1)) end
|
|
|
|
(** 4. With effects and a reference as argument *)
|
|
|
|
let rec f4 (a:ref int) : unit variant { !a }
|
|
requires { !a >= 0 } ensures { !x = old !x + old !a }
|
|
= if !a > 0 then begin x := !x + 1; a := !a - 1; f4 a end
|
|
|
|
(** 5. The acid test:
|
|
partial application of a recursive function with effects *)
|
|
|
|
let rec f5 (a b:ref int) variant { !a }
|
|
requires { !a >= 0 } ensures { result = old !a + old !b }
|
|
= if !a = 0 then !b else begin a := !a - 1; b := !b + 1; f5 a b end
|
|
|
|
let test_f5 () requires { !x >= 0 } ensures { result = old !x }
|
|
= let b = ref 0 in let f = f5 x in f b
|
|
|
|
end
|