Hi,
I'd like to understand better the meaning of the "writes" annotation in recent
versions of Why3 (I'm running Why3 platform, version 0.87.3)
So far, I understand that :
1) on a val, a writes annotation specifies the effect of the val on its
(mutable) arguments.
2) on a val, not using any wr
Hi Delphine,
On 2 March 2018 at 15:37, Delphine Demange
wrote:
> Hi,
>
> I'd like to understand better the meaning of the "writes" annotation in
> recent versions of Why3 (I'm running Why3 platform, version 0.87.3)
>
> So far, I understand that :
> 1) on a val, a writes annotation specifies the
