KeYProject
Logical Infrastructure for final values independent from the heap
This is a copy of Merge Request !318 at gitlab. See also there for an extensive discussion on the subject.
Constructors
This mechanism must not be used when verifying a constructor or if constructors are planned to be inlined. In these cases, final field are writable. We suggest to implement this mechanism with a taclet option such that it can be switched off -- or even switched off automatically if need be.
Example
This file that can be closed automatically with this encoding. It cannot be closed in KeY itself since the final modifier is not considered in KeY.
A.java
Remaining issues
This is work in progress. There may be parts of KeY where this change has unexpected consequences.
- [ ] Make it a taclet option
- [ ] Add documentation to new methods
- [ ] OPTIONAL: Adapt welldefined checking. @mi-ki
- [ ] OPTIONAL: Add a class
FinalArray<T>which allows this for arrays too (well ...)
Side note: The variable condition \final has already been implemented by Daniel, but was not used till now. Thanks.
Does this also affect the proof management tool of @WolframPfeifer? Checking whether taclet option was active, while a constructor appeared in a method-frame?
This PR has been superseded by #3495 based on the same (but rebased) code changes