On Mon, 8 Apr 2019, Jean-Christophe Filliatre wrote:
>
> >> 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?
>
> The call site receives two integers, the second being ghost. You can
> bind them as follows:
>
> let x, g = f 42 in
> ...
>
> Whenever you extract your code to OCaml, ghost code will be erased and
> this will be turned into a "let" binding only x.
Actually, in my case, there is no real return value. So I kind of balk at
having to put a let, where there is no real return value. The calling
context doesn't care about the ghost, only the ensures. But in the
interest of progressing, I'll go with the let.
>
> > 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.
>
> Syntactically, any expression can be followed by an "ensures". A
> function body makes no exception. And there is a VC to prove that
> "ensures" as part of the function's VCs.
>
> In the particular case of an "ensures" put on a function body, Why3
> makes some effort to turn it into a function contract, when possible.
> Consider the following two functions:
>
> let f1 (x: int) : int
> = let x = ref 0 in x := 40; !x + 2 ensures { !x + 2 = 42 }
>
> let f2 (x: int) : int
> = let x = ref 40 in !x + 2 ensures { !x + 2 = 42 }
>
> In the case of f1, you won't get the "ensures" at the call site. In the
> case of f2, you will.
The difference is that the second has no externally visible side effects?
Unfortunately, that is not the case for my code.
thanks,
julia
> --
> Jean-Christophe
> _______________________________________________
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
