Improved treatment of final fields

[mattulbrich]

Intended Change

Final fields cannot change their value after a single assignment in the constructor. In the current KeY logic, final fields are treated like normal fields stored on the heap. This is highly inefficient since heap assignments cannot have an impact on final fields at all.

The plan is hence to access final fields using a function of their own that does not depend on the heap, unlike other fields

T::select(Heap, Object, Field)   // for non-static fields
T::final(Object, Field)  // for static fields

The major challenges include

• adapting reading of final fields in modalities
• adapting accessing final fields in JML
• handling constructors: they are allowed to write.

Writing must somehow be restricted since any modality could write to final fields and thus compromise proofs if thus different inconsistent values for final fields are around on a sequent.

Plan

• [x] Add functions for finals, add a taclet option
• [x] Implement rules that act upon those taclet options
• [ ] Implement special treatment for constructors
• [ ] Test effectiveness
• [ ] Code cleanup
• [ ] Document the changes

Type of pull request

• Breaking change (feature that cause existing functionality to change)

The plan is to have a taclet otion to fall back to old behaviour.

Ensuring quality

To do:

• 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.
• I have tested the feature as follows: ...
• I have checked that runtime performance has not deteriorated.

Additional information and contact(s)

It is the modernised version of #3189.

@WolframPfeifer @wadoon

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.