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

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

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.


Why3-club mailing list

Reply via email to