On Sun, 7 Apr 2019, Mario Pereira wrote:
> Hello,
>
> I believe you can resort to *ghost results* in order to solve this
> issue. In Why3, a function can return multiple results, some of them
> marked as ghost.
>
> For instance:
>
> let f (x: int) : (r: int, ghost rg: int)
> ensures { r = rg + 1 /\ rg = x }
> = (x+1, x)
>
> Generally speaking, whenever you need to quantify existentially in a
> postcondition you might consider return a witness, in the form of a
> ghost result.
So the call site just receives an integer, and not a pair of an integer
and a ghost integer?
It seems that I can put an ensures at the end of the function as well, and
it can refer to a variable that is let bound in the first line. But I
haven't checked whether that ensures is available to the call site.
julia_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
