On 9 November 2016 at 15:26, Jean-Jacques Levy
wrote:
> But:
>
>let f (x: int) (ghost y: int) (ghost dy: ref int) = dy := y; x
>
> is no longer applicative programming style.. You have side effect.
Of course, I do.
A.
>> Le 9 nov. 2016 à 15:18, Andrei Paskevich a écrit :
>>
>> Dear Jean-Ja
But:
let f (x: int) (ghost y: int) (ghost dy: ref int) = dy := y; x
is no longer applicative programming style.. You have side effect.
-JJ-
> Le 9 nov. 2016 à 15:18, Andrei Paskevich a écrit :
>
> Dear Jean-Jacques,
>
> On 9 November 2016 at 11:49, Jean-Jacques Levy
> wrote:
>> what is b
On 9 November 2016 at 15:18, Andrei Paskevich wrote:
> In the development version, it is possible for a non-ghost function to
> return tuples with ghost components.
And, to be precise, the "development version" here means the branch
called "new_system" in the git repository of Why3.
A.
_
Dear Jean-Jacques,
On 9 November 2016 at 11:49, Jean-Jacques Levy
wrote:
> what is best way of having a ghost component in the results of functions ?
>
> A record with a ghost field as a return value of a function seems accepted by
> why3.
>
> type rr = { dx: int; ghost dy : int}
> let f (x
Dear Why3 Friends,
what is best way of having a ghost component in the results of functions ?
A record with a ghost field as a return value of a function seems accepted by
why3.
type rr = { dx: int; ghost dy : int}
let f (x: int) (ghost y: int) = {dx = x; dy = y}
A tuple with a ghost co
