Hi Delphine,

On 2 March 2018 at 15:37, Delphine Demange <delphine.dema...@irisa.fr>

> 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.


> 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

> 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

Why3-club mailing list

Reply via email to