mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
20 lines
372 B
Plaintext
20 lines
372 B
Plaintext
|
|
module LocalFunctions
|
|
|
|
use int.Int
|
|
use ref.Ref
|
|
|
|
(* local function (f) accessing a local reference (x) *)
|
|
let test1 () =
|
|
let x = ref 0 in
|
|
let f (y: int) ensures { !x = old !x + y } = x := !x + y in
|
|
f 2;
|
|
assert { !x = 2 }
|
|
|
|
val r: ref int
|
|
|
|
(* recursive function accessing a global reference *)
|
|
let rec test2 () ensures { !r = 0 } = r := 0
|
|
|
|
end
|