Documentation for Treatment of Final Fields

[WolframPfeifer]

There is a new treatment of final fields about to be merged into main KeY (KeYProject/key#3495).

I think it is a good idea to write a user documentation about it.

Here are some ideas and questions what to describe in the docs:

Treatment of Final Fields

Motivation

• Why is it a good idea to have a special treatment for final fields in KeY?
• Maybe give some statistics/insights about the effect of that feature on case study?
• Reference to the STTT journal paper (as soon as it appears)? (Not sure if there are differences to what is described here ...)

Recap: Final fields in Java

• Maybe add a quick recap on where final fields can be written/accessed in Java (that is quite an edge case and not something I was entirely sure of, not even as a Java developer)?

The Solution for KeY

• new (sort-depending) function symbol in logic

• changed default, taclet option for legacy treatment

• Difference between the two settings?

• Soundness/completeness?

  • user guideline when to use which of the two options

• What exactly does the static analysis check for?

• How does the new feature interact with inlining?

• How does this feature work with static fields?

• Does the feature work for ghost fields as well?

• What are examples for critical edge cases that we have to mitigate (reading before writing the final field)?

• How is the new symbol printed in pretty-printing? How can it be distinguished from the normal select?

• Are there any known current limitations or open questions (inner classes maybe)?

[WolframPfeifer]

@mattulbrich Here is the list with questions you wanted to have ...