What is the difference between modifies this, modifies this.x, and modifies this`x?
What is the difference between
modifies this.x, and
modifies clause for a method lists object references whose fields may be modified by the body of the method.
thismeans that all the fields of the
thisobject may be modified by the body
xis a field of
thisand has some reference type) means that fields of
xmay be modified (but not the field
this`xmeans that just the field
thismay be modified (and not any other fields, unless they are listed themselves)
If there are multiple items listed in the modifies clause, the implicit clause is the union of all of them.
More on framing (
reads clauses) can be found in the reference manual section on Framing specifications.