Hi Delphine,

On 2 March 2018 at 15:37, Delphine Demange <delphine.dema...@irisa.fr>
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 effect of the val on its
> (mutable) arguments.
>

Correct. Both on mutable arguments and external mutable variables.


> 2) on a val, not using any writes annotation means that the val function
> *doesn't modify* its arguments. Not writing any writes is the same as
> saying writes { } :  it has no visible effect.
>

Correct.


> 3) on a let function, it's absence / presence is not so important : why3
> can infer the effect of the let, even if the let doesn't have any writes
> annotation, or have incomplete writes annotations.
>

Correct. Though, if a "write" effect is given, why3 should warn you if it
is not the same as the inferred one.


> Do I understand it correctly?
> Could you point me to some document explaining that kind of considerations?
>

To my knowledge, there is no such document atm and we should start writing
one.


> I find item 2) surprising.
> At first, I was expecting that not specifying the effect would be like not
> specifying the ensures, i.e. everything can happen, and we don't know
> anything about the val.
>

This would make sense for mutable arguments but not for external mutable
variables (how should we choose which ones get havoc'd?). Though I agree
that the current semantics is not the safest by default, and your idea is
worth adopting, if we find a reasonable "pessimist" footprint for external
variables.

Best,
Andrei
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

Reply via email to