Proof Scripts in JML

[mattulbrich]

Related Issue

For quite some time, we have a prototype for JML proof scripts which we finally want to bring to the mater branch.

Intended Change

Proof scripts can be written into JML comments and can be obeyed during automatic verification.
The major benefit is that the localisation of the proof node to which a proof script should be applied is natural.
The other benefit is that one can use JML expressions and thus does not have to leave the realm of JML to do script-guided proofs.

This relies on #3587 and needs #3654 merged.

Plan

• Refine the syntax
• Adapt lexer and parser
• Reimport the implementation that was available on an older branch
• Make it more convenient
• Add examples
• Code cleanup
• Document the changes

Type of pull request

• New feature (non-breaking change which adds functionality)
• There are changes to the (Java) code
• There are changes to the taclet rule base (possibly small adaptations)

Ensuring quality

WIP:

• 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: ... examples and test cases
• I have checked that runtime performance has not deteriorated. not for non-script proofs.

Additional information and contact(s)

Planned to be done Mid 09/25

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

[codecov]

Codecov Report

❌ Patch coverage is 0% with 40 lines in your changes missing coverage. Please review.
✅ Project coverage is 37.14%. Comparing base (e5853a5) to head (ff1ce97).
⚠️ Report is 78 commits behind head on main.

Files with missing lines	Patch %	Lines
...src/main/java/org/key_project/logic/PosInTerm.java	0.00%	13 Missing ⚠️
...rc/main/java/org/key_project/util/java/IOUtil.java	0.00%	11 Missing ⚠️
.../org/key_project/util/collection/ImmutableSet.java	0.00%	5 Missing ⚠️
...ain/java/org/key_project/util/java/StringUtil.java	0.00%	5 Missing ⚠️
...org/key_project/util/collection/ImmutableList.java	0.00%	3 Missing ⚠️
...in/java/org/key_project/util/java/IntegerUtil.java	0.00%	3 Missing ⚠️

❗ There is a different number of reports uploaded between BASE (e5853a5) and HEAD (ff1ce97). Click for more details.

HEAD has 4 uploads less than BASE

Flag	BASE (e5853a5)	HEAD (ff1ce97)
	14	10

Additional details and impacted files

@@              Coverage Diff              @@
##               main    #3657       +/-   ##
=============================================
- Coverage     47.98%   37.14%   -10.85%     
+ Complexity    16045      760    -15285     
=============================================
  Files          1683      129     -1554     
  Lines         96046     5689    -90357     
  Branches      15388      897    -14491     
=============================================
- Hits          46091     2113    -43978     
+ Misses        44683     3387    -41296     
+ Partials       5272      189     -5083     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

[wadoon]

I have written an integer split command.

An induction command is on the way with support for int, user-data types, bsum(?).

Commit: 4644331

[wadoon]

@WolframPfeifer Could you please revert the merge of main into this PR (and do a rebase instead, or just let to @mattulbrich for the sake of confusion avoidance)?

This was a merge-free PR, which results in an easier-to-read git history.

[WolframPfeifer]

@WolframPfeifer Could you please revert the merge of main into this PR (and do a rebase instead, or just let to @mattulbrich for the sake of confusion avoidance)?

This was a merge-free PR, which results in an easier-to-read git history.

Ok, I reverted the merge. I see the point about a clean history. However, I am not sure what a good workflow would be. Should we do a merge with main only at the end of the feature development, before the merge of the PR?