There is an unsaved comment in progress. You will lose your changes if you continue. Are you sure you want to reopen the work item?
Finer-grained writes clauses
If f is a field of an object o, we should give a meaning to a writes clause of the form
It would be convenient, if this writes clause would allow unwrapping o but not changing any other field than f (plus, of course, the corresponding framing on the caller's side). This would allow to safe a lot of \unchanged(...) post-conditions for all those fields that did not change.