why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2020-06-23T18:50:33+02:00https://gitlab.inria.fr/why3/why3/-/issues/490Function symbol not found in a block of mutually recursive definitions2020-06-23T18:50:33+02:00Mário PereiraFunction symbol not found in a block of mutually recursive definitionsConsider the following example:
```
let rec function f (x: int)
ensures { result = g x }
=
g x
with function g (x: int) =
f x
```
Why3 complains with an unbound function error for the postcondition of `f`. Is this the expected beh...Consider the following example:
```
let rec function f (x: int)
ensures { result = g x }
=
g x
with function g (x: int) =
f x
```
Why3 complains with an unbound function error for the postcondition of `f`. Is this the expected behavior? Since `g` is defined using `with function`, I supposed it would be bound also for the contract of `f`.https://gitlab.inria.fr/why3/why3/-/issues/393type invariant preservation question2019-11-27T13:19:54+01:00DAILLER Sylvaintype invariant preservation questionI 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 t...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
```