Introduce JML aliases of frame conditions for better tool compatibility

[mi-ki]

This pull request allows handling various aliases for frame conditions within method/block/loop contracts and loop specifications. These aliases cover the ones which are used in various other verification tools with contracts for Java-like programs, e.g., Krakatoa, OpenJML, Dafny, ACSL++, or CorC.

In particular, the following aliases are henceforth supported for frame conditions in method, block, and loop contracts as well as loop specifications:

assignable, assigns, assigning, modifiable, modifies, modifying, writable, writes, writing.

Upon usage of the italic versions, we throw a warning in order to distinguish expected semantics, e.g., from runtime verification, as KeY does static analysis, but (other than potentially seeing a warning) these versions are supported in the same way as the other aliases.

For loop specifications, we also support the respective aliases with the prefix loop_.

During discussions on this pull request, it was noted that the semantics implemented within KeY might be better captured by modifiable, but for legacy reasons, we do not move away from (also) using assignable.

Related Issue

This pull request addresses #3362.

Intended Change

This pull request introduces the aliases for frame conditions which are shown above. Thereby, it increases compatibility with further tools using JML, JML variants, or JML-alikes, such as Krakatoa, OpenJML, Dafny, or ACSL++.

Type of pull request

• [ ] Bug fix (non-breaking change which fixes an issue)
• [ ] Refactoring (behavior should not change or only minimally change)
• [x] New feature (non-breaking change which adds functionality)
• [ ] Breaking change (fix or feature that would cause existing functionality to change)
• [x] There are changes to the (Java) code
• [ ] There are changes to the taclet rule base
• [ ] There are changes to the deployment/CI infrastructure (gradle, github, ...)
• [ ] Other:

Ensuring quality

• [ ] I made sure that introduced/changed code is well documented (Javadoc and inline comments).
• [ ] I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
• [ ] I added new test case(s) for new functionality.
• [x] I have tested the feature as follows: Checked it for the example from the referenced issue.
• [ ] I have checked that runtime performance has not deteriorated.

Additional information and contact(s)

Some of the changes are results from work at the HacKeYthon together with @unp1. The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.