type invariant preservation question
I have a quite simple question about the behavior of type invariant. In the simple program below, I am asked by the tool to prove a type invariant inside function g
for variable e
(after split). I would have expected this invariant to be ensured in the proof for f
. Is there a way to tell the tool "at this point of program type invariants should hold" ?
module Example
type r = { mutable p: int }
invariant { p = 42 }
let f (e: r)
writes {e}
ensures { true }
=
e.p <- 42
let g ()
diverges
=
let e: r = { p = 42 } in
while true do
f (e);
done
end