Forbid write and readwrite on pre variable

[ptal]

For example: pre x.inc() should not be valid because the method inc modifies the variable x.

We chose to specify read/write attributes on the variables because we did not want to impact the Java signature of a method (that might not be inside the current project) or add wrappers around these methods to specify these attributes.
However this static analysis would be more easily done if we have read/write attributes on the methods themselves.
Another possibility is to force the user to write pre read x.inc() although with pre it is already implied.
(Note that it does not solve the problem that the user can lie about the Java signature...).

[ptal]

A simpler solution is to forbid calling methods on pre variables. Although it is easy to bypass by wrapping the call in host functions.