Proof Scripts in JML by mattulbrich · Pull Request #3657 · KeYProject/key

mattulbrich · 2025-09-08T19:13:22Z

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

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.

(cherry-picked from earlier attempt to implement JML proof scripts) # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JMLTransformer.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JmlAssert.java # key.core/src/main/java/de/uka/ilkd/key/java/statement/JmlAssert.java # key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLAssertStatement.java # key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java

…aDL arguments) (cherry-picked from earlier attempt to implement JML proof scripts)

(cherry-picked from earlier attempt to implement JML proof scripts)

# Conflicts: # key.core/src/main/java/de/uka/ilkd/key/logic/Semisequent.java # key.core/src/main/java/de/uka/ilkd/key/scripts/RuleCommand.java # key.core/src/main/java/de/uka/ilkd/key/scripts/SetCommand.java # key.core/src/main/java/de/uka/ilkd/key/strategy/StrategyProperties.java

(cherry-picked from earlier attempt to implement JML proof scripts)

(cherry-picked from earlier attempt to implement JML proof scripts) # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java

codecov · 2025-09-08T19:14:36Z

Codecov Report

❌ Patch coverage is 0% with 42 lines in your changes missing coverage. Please review.
✅ Project coverage is 37.12%. Comparing base (28025d8) to head (16e79e7).
⚠️ Report is 160 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%	7 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 (28025d8) and HEAD (16e79e7). Click for more details.

HEAD has 4 uploads less than BASE

Flag BASE (28025d8) HEAD (16e79e7)

14 10

Additional details and impacted files

@@              Coverage Diff              @@
##               main    #3657       +/-   ##
=============================================
- Coverage     47.16%   37.12%   -10.04%     
+ Complexity    15801      760    -15041     
=============================================
  Files          1673      129     -1544     
  Lines         96171     5691    -90480     
  Branches      15397      897    -14500     
=============================================
- Hits          45359     2113    -43246     
+ Misses        45641     3389    -42252     
+ Partials       5171      189     -4982

☔ 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.

key.core/src/main/antlr4/JmlParser.g4

wadoon · 2025-09-09T02:15:30Z

I have written an integer split command.

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

Commit: 4644331

…her goals, print position manual cherry-pick From 547ce29 Mon Sep 17 00:00:00 2001 From: Julian Wiesler <wiesleju@gmail.com> Date: Wed, 22 Feb 2023 13:57:21 +0100 Subject: [PATCH] Position info for scripts with url=null, run scripted goals before other goals, print position information

…o since it splits a lot better # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java

manual cherry-picking commit 886588a Author: Mattias Ulbrich <ulbrich@kit.edu> Date: Sun Feb 5 13:14:29 2023 +0100

manually cherry-picked from old branch

adapted to new branch by MU

solution by Alexander Weigl

wadoon · 2026-02-03T14:46:22Z

@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 · 2026-02-06T11:36:47Z

@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?

wadoon · 2026-02-23T12:22:12Z

35160      DEBUG Test worker     d.u.i.k.s.ProofScriptEngine Commands: macro  "autopilot-prep";
tryclose  ;
macro  "simp-upd";
rule  seqPermFromSwap;
rule  andRight;
auto  ;
instantiate with: (i_0) var: "iv" hide;
instantiate with: j_0 var: jv hide;
auto  ;
macro  "simp-upd";
rule  seqPermFromSwap;
rule  andRight;
auto  ;
instantiate with: (i_0) var: "iv" hide;
instantiate with: (to) var: "jv" hide;
auto  ; 

Error while executing script: Could not convert value 'j_0' from type 'ProofScriptExpressionContext' to type 'JTerm'

Command: instantiate with: j_0 var: jv hide;
Position: [file:/home/weigl/work/key/key.core/../key.ui/examples/heap/quicksort/split.key:30/2]

de.uka.ilkd.key.scripts.ScriptException: Error while executing script: Could not convert value 'j_0' from type 'ProofScriptExpressionContext' to type 'JTerm'

Command: instantiate with: j_0 var: jv hide;
Position: [file:/home/weigl/work/key/key.core/../key.ui/examples/heap/quicksort/split.key:30/2]

	at de.uka.ilkd.key.scripts.ProofScriptEngine.execute(ProofScriptEngine.java:162)
	at de.uka.ilkd.key.scripts.ProofScriptEngine.execute(ProofScriptEngine.java:80)
	at de.uka.ilkd.key.proof.runallproofs.ProveTest.autoMode(ProveTest.java:194)

5028      INFO  Test worker     d.u.i.k.p.r.ProveTest     (parallelGcd.proof|1412243253) Proof will be saved to: /home/weigl/work/key/key.core/../key.ui/examples/heap/verifyThis15_2_ParallelGcd/parallelGcd.proof.proof 
25028      INFO  Test worker     d.u.i.k.p.r.ProveTest     (parallelGcd.proof|1412243253) Start proving 
25028      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /home/weigl/work/key/key.core/../key.ui/examples/heap/verifyThis15_2_ParallelGcd/parallelGcd.proof 
25028      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.53ns 
25030      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26664      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 1.63s 
26895      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 194.78ms 
26895      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replay result: Proof replayed successfully.Errors while reading the proof. Not all branches could be load successfully. 
26896      INFO  Test worker     d.u.i.k.p.r.ProveTest     (parallelGcd.proof|1412243253) Proving done 

Loading problem file failed
Expected :false
Actual   :true
<Click to see difference>

Macro 'script-auto' raised an exception: Error while executing script: Multiple or no formulas modified or added in last step, cannot identify sequent formula to skolemize.

Command: __obtain from_goal: true var: x ;
Position: [file:/home/weigl/work/key/key.core/../key.ui/examples/heap/BoyerMoore/src/BoyerMoore.java:74/18]

de.uka.ilkd.key.scripts.ScriptException: Macro 'script-auto' raised an exception: Error while executing script: Multiple or no formulas modified or added in last step, cannot identify sequent formula to skolemize.

Command: __obtain from_goal: true var: x ;
Position: [file:/home/weigl/work/key/key.core/../key.ui/examples/heap/BoyerMoore/src/BoyerMoore.java:74/18]

	at app//de.uka.ilkd.key.scripts.MacroCommand.execute(MacroCommand.java:117)
	at app//de.uka.ilkd.key.scripts.AbstractCommand.execute(AbstractCommand.java:79)
	at app//de.uka.ilkd.key.scripts.ProofScriptEngine.execute(ProofScriptEngine.java:129)
	at app//de.uka.ilkd.key.scripts.ProofScriptEngine.execute(ProofScriptEngine.java:80)
	at app//de.uka.ilkd.key.proof.runallproofs.ProveTest.autoMode(ProveTest.java:194)
	at app//de.uka.ilkd.key.proof.runallproofs.ProveTest.runKey(ProveTest.java:135)
	at app//de.uka.ilkd.key.proof.runallproofs.ProveTest.assertProvability(ProveTest.java:63)
	at app//de.uka.ilkd.key.proof.runallproofs.gen._example_algos.testBM_bm(_example_algos.java:36)
	at java.base@25.0.2/java.lang.reflect.Method.invoke(Method.java:565)
	at java.base@25.0.2/java.util.ArrayList.forEach(ArrayList.java:1604)
	at java.base@25.0.2/java.util.ArrayList.forEach(ArrayList.java:1604)
Caused by: de.uka.ilkd.key.scripts.ScriptException: Error while executing script: Multiple or no formulas modified or added in last step, cannot identify sequent formula to skolemize.

Command: __obtain from_goal: true var: x ;
Position: [file:/home/weigl/work/key/key.core/../key.ui/examples/heap/BoyerMoore/src/BoyerMoore.java:74/18]

	at app//de.uka.ilkd.key.scripts.ProofScriptEngine.execute(ProofScriptEngine.java:162)
	at app//de.uka.ilkd.key.macros.ApplyScriptsMacro.applyTo(ApplyScriptsMacro.java:210)
	at app//de.uka.ilkd.key.macros.AbstractProofMacro.applyTo(AbstractProofMacro.java:72)
	at app//de.uka.ilkd.key.macros.SequentialProofMacro.applyTo(SequentialProofMacro.java:99)
	at app//de.uka.ilkd.key.macros.AbstractProofMacro.applyTo(AbstractProofMacro.java:72)
	at app//de.uka.ilkd.key.scripts.MacroCommand.execute(MacroCommand.java:113)
	... 10 more
Caused by: java.lang.IllegalStateException: Multiple or no formulas modified or added in last step, cannot identify sequent formula to skolemize.
	at de.uka.ilkd.key.scripts.ObtainCommand.identifySequentFormula(ObtainCommand.java:139)
	at de.uka.ilkd.key.scripts.ObtainCommand.executeFromGoal(ObtainCommand.java:91)
	at de.uka.ilkd.key.scripts.ObtainCommand.execute(ObtainCommand.java:77)
	at de.uka.ilkd.key.scripts.AbstractCommand.execute(AbstractCommand.java:79)
	at de.uka.ilkd.key.scripts.ProofScriptEngine.execute(ProofScriptEngine.java:129)
	... 15 more

mattulbrich added 6 commits September 8, 2025 21:05

first working example of a proof script in Java code (albeit with Jav…

740b046

…aDL arguments) (cherry-picked from earlier attempt to implement JML proof scripts)

added missing files for script aware macros

0527387

(cherry-picked from earlier attempt to implement JML proof scripts)

more infrastructure for proof scripts

751d117

(cherry-picked from earlier attempt to implement JML proof scripts)

more infrastructure for proof scripts

0a401af

(cherry-picked from earlier attempt to implement JML proof scripts) # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java

mattulbrich added JavaJMLParser JML (Semantics) P:HIGH Proof Scripts labels Sep 8, 2025

mattulbrich added 3 commits September 8, 2025 21:16

adapting to new Script AST nodes

c00284e

renaming AssertCommand to FailUnlessCommand

ca3711b

correcting the grammar for nested \by clauses

e6c2ed9

wadoon self-requested a review September 8, 2025 23:22

wadoon assigned mattulbrich Sep 8, 2025

wadoon added this to the v2.12.4 milestone Sep 8, 2025

wadoon reviewed Sep 9, 2025

View reviewed changes

key.core/src/main/antlr4/JmlParser.g4 Show resolved Hide resolved

mattulbrich added 11 commits September 10, 2025 19:11

improving the value injector

dc898e8

renaming a deprecated command "assert" --> "assertOpenGoals"

11672e5

spotless

a0a225a

working version of scripts

c506ab6

Use AutoPilotPrepareProofMacro instead of FinishSymbolicExecutionMacr…

66c4056

…o since it splits a lot better # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java

working on improved script commands

8c416b1

manual cherry-picking commit 886588a Author: Mattias Ulbrich <ulbrich@kit.edu> Date: Sun Feb 5 13:14:29 2023 +0100

advancing the immutable list interface

5e15b3e

reorganisation of proof script commands

5ae4c95

manually cherry-picked from old branch

advancing for scripts from JML

a825b96

slight adaptation of the macro used for scripting

94dac2f

mattulbrich and others added 3 commits October 11, 2025 01:27

bugfixing matching with program variables

aacfba1

updating the focus rule

77e361f

allow terms with holes in expand command

25d2b79

adapted to new branch by MU

mattulbrich force-pushed the jmlScripts branch from 23fa08e to 2066973 Compare October 10, 2025 23:55

added convenience macro to close all NPE and Out-of-bounds branches

ae8b141

mattulbrich force-pushed the jmlScripts branch from 2066973 to ae8b141 Compare October 11, 2025 00:01

mattulbrich marked this pull request as ready for review October 11, 2025 00:11

mattulbrich added the Review Request Waiting for review label Oct 11, 2025

mattulbrich requested a review from WolframPfeifer October 11, 2025 00:11

mattulbrich added 3 commits October 11, 2025 13:46

bug fixes in script engine

a09d684

repairing JML script tests

3bb4332

fixing a NPE bug in JavaProfile

2bc3a36

solution by Alexander Weigl

mattulbrich force-pushed the jmlScripts branch from 07792f4 to 2bc3a36 Compare October 15, 2025 08:07

improving symbex only macro

46567da

mattulbrich force-pushed the jmlScripts branch from d5d10bf to 46567da Compare October 24, 2025 13:22

adding an infinity catch on "throw null" in symb ex.

ec5929d

WolframPfeifer modified the milestones: v2.13.0, v3.0.0 Jan 7, 2026

WolframPfeifer force-pushed the jmlScripts branch from ff1ce97 to ec5929d Compare February 6, 2026 11:26

mattulbrich and others added 7 commits February 17, 2026 21:43

making the assume command use a local taclet.

4f4b4b0

correcting conversion in JML scripts

30efd94

adapting taclets.old.txt to changed throws treatment

2b3ab15

Repaired a merge test case

20a6513

missing sameUpdateLevel for tryCatchThrow

aa375ba

spotless

d076cef

fix regression fixtures taclets.old.txt

8668a0a

fixing empty qualifier

16e79e7

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Comments

Proof Scripts in JML#3657

Proof Scripts in JML#3657
mattulbrich wants to merge 85 commits intoKeYProject:mainfrom
mattulbrich:jmlScripts

mattulbrich commented Sep 8, 2025 •

edited

Loading

Uh oh!

codecov bot commented Sep 8, 2025 •

edited

Loading

Uh oh!

Uh oh!

wadoon commented Sep 9, 2025

Uh oh!

wadoon commented Feb 3, 2026

Uh oh!

WolframPfeifer commented Feb 6, 2026

Uh oh!

wadoon commented Feb 23, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Comments

Conversation

mattulbrich commented Sep 8, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Related Issue

Intended Change

Plan

Type of pull request

Ensuring quality

Additional information and contact(s)

Uh oh!

codecov bot commented Sep 8, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

Uh oh!

wadoon commented Sep 9, 2025

Uh oh!

wadoon commented Feb 3, 2026

Uh oh!

WolframPfeifer commented Feb 6, 2026

Uh oh!

wadoon commented Feb 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

mattulbrich commented Sep 8, 2025 •

edited

Loading

codecov bot commented Sep 8, 2025 •

edited

Loading

wadoon commented Feb 23, 2026 •

edited

Loading