Contracts and non private, non final fields

Fields cannot be annotated. This means that non-final protected, package-local or public fields may be modified from the outside causing contract violations.

Two possibilities:

• Ignore. Making non-final fields anything other than private is bad style anyway.

• Allow to annotate fields. This may have a serious performance impact.