Proof Scripts in JML#3657

Open

mattulbrich wants to merge 101 commits into

KeYProject:mainfrom

mattulbrich:jmlScripts

Commits on May 6, 2026

first steps to allow scripts in jml

mattulbrich
authored and
wadoon
committed
first working example of a proof script in Java code (albeit with JavaDL arguments)

mattulbrich
authored and
wadoon
committed
added missing files for script aware macros

mattulbrich
authored and
wadoon
committed
more infrastructure for proof scripts

mattulbrich
authored and
wadoon
committed
more infrastructure for proof scripts

mattulbrich
authored and
wadoon
committed
more infrastructure for proof scripts

mattulbrich
authored and
wadoon
committed
adapting to new Script AST nodes

mattulbrich
authored and
wadoon
committed
renaming AssertCommand to FailUnlessCommand

mattulbrich
authored and
wadoon
committed
correcting the grammar for nested \by clauses

mattulbrich
authored and
wadoon
committed
improving the value injector

mattulbrich
authored and
wadoon
committed
renaming a deprecated command "assert" --> "assertOpenGoals"

mattulbrich
authored and
wadoon
committed
spotless

mattulbrich
authored and
wadoon
committed
working version of scripts

mattulbrich
authored and
wadoon
committed
Position info for scripts with url=null, run scripted goals before other goals, print position

mattulbrich
authored and
wadoon
committed
Use AutoPilotPrepareProofMacro instead of FinishSymbolicExecutionMacro since it splits a lot better

mattulbrich
authored and
wadoon
committed
working on improved script commands

mattulbrich
authored and
wadoon
committed
advancing the immutable list interface

mattulbrich
authored and
wadoon
committed
reorganisation of proof script commands

mattulbrich
authored and
wadoon
committed
advancing for scripts from JML

mattulbrich
authored and
wadoon
committed
slight adaptation of the macro used for scripting

mattulbrich
authored and
wadoon
committed
more script commands

mattulbrich
authored and
wadoon
committed
improving/correcting script commands

mattulbrich
authored and
wadoon
committed
settings for the auto command

mattulbrich
authored and
wadoon
committed
propagating strategy settings to the strategy to be used

mattulbrich
authored and
wadoon
committed
proof scripts: adding a CHEAT command

mattulbrich
authored and
wadoon
committed
updating a few of the script commands

mattulbrich
authored and
wadoon
committed
introducing the script-aware prep macro

mattulbrich
authored and
wadoon
committed
issue dialog: skip spaces for squiggly lines

mattulbrich
authored and
wadoon
committed
value injector: towards reporting unknown arguments

mattulbrich
authored and
wadoon
committed
improved script error reporting

mattulbrich
authored and
wadoon
committed
documentation for script commands

mattulbrich
authored and
wadoon
committed
better error messaging in ScriptLineParser

mattulbrich
authored and
wadoon
committed
implement a recall mechanism

mattulbrich
authored and
wadoon
committed
allow let commands without "@"

mattulbrich
authored and
wadoon
committed
a formula parameter for the expand command

mattulbrich
authored and
wadoon
committed
spotlessing

mattulbrich
authored and
wadoon
committed
towards 'obtain' in JML scripts

mattulbrich
authored and
wadoon
committed
update ProofScriptEngine's workflow

mattulbrich
authored and
wadoon
committed
consolidating, introducing test cases for jml scripts

mattulbrich
authored and
wadoon
committed
first working obtain scripts

mattulbrich
authored and
wadoon
committed
pimping the document generation for proof script commands

mattulbrich
authored and
wadoon
committed
lots of script documentation

mattulbrich
authored and
wadoon
committed
fixing a bug regarding proof script application

mattulbrich
authored and
wadoon
committed
repairing some weird self variable treatment in SpecStatement

mattulbrich
authored and
wadoon
committed
introducing "auto add_*" to scripts.

mattulbrich
authored and
wadoon
committed
smaller fixes in proof script treatment

mattulbrich
authored and
wadoon
committed
The Boyer-Moore example now runs on scripts

mattulbrich
authored and
wadoon
committed
improved document generation

mattulbrich
authored and
wadoon
committed
more proof script power, update inlining.

mattulbrich
authored and
wadoon
committed
making sure that cuts work with boolean terms instead of formulas.

mattulbrich
authored and
wadoon
committed
better symbex-only machine

mattulbrich
authored and
wadoon
committed
Allowing "auto only: ..."

mattulbrich
authored and
wadoon
committed
quicksort example with JML scripts (partially)

mattulbrich
authored and
wadoon
committed
enabling the quicksort example with JML proof scripts!

mattulbrich
authored and
wadoon
committed
limiting the symbex only macro a bit

mattulbrich
authored and
wadoon
committed
introducing hole placeholders for terms and for formulas

mattulbrich
authored and
wadoon
committed
introducing witness command

mattulbrich
authored and
wadoon
committed
adapting the cherry-picked commits

mattulbrich
authored and
wadoon
committed
allowing switching off rules in auto

mattulbrich
authored and
wadoon
committed
a more robust term-with-holes implementation

mattulbrich
authored and
wadoon
committed
improved treatment of terms with holes

mattulbrich
authored and
wadoon
committed
introduce match identifiers with leading '?'

mattulbrich
authored and
wadoon
committed
introducing sort::FOCUS for usage in scripts

mattulbrich
authored and
wadoon
committed
introducing sort::ELLIP for ellipsis search patterns

mattulbrich
authored and
wadoon
committed
improving sophisticated term matching

mattulbrich
authored and
wadoon
committed
accomodating "focus inside find"

mattulbrich
authored and
wadoon
committed
add "assumes" parameter to rule command

mattulbrich
authored and
wadoon
committed
bugfixing matching with program variables

mattulbrich
authored and
wadoon
committed
updating the focus rule

mattulbrich
authored and
wadoon
committed
allow terms with holes in expand command

WolframPfeifer
authored and
wadoon
committed
added convenience macro to close all NPE and Out-of-bounds branches

WolframPfeifer
authored and
wadoon
committed
bug fixes in script engine

mattulbrich
authored and
wadoon
committed
repairing JML script tests

mattulbrich
authored and
wadoon
committed
fixing a NPE bug in JavaProfile

mattulbrich
authored and
wadoon
committed
improving symbex only macro

mattulbrich
authored and
wadoon
committed
adding an infinity catch on "throw null" in symb ex.

mattulbrich
authored and
wadoon
committed
making the assume command use a local taclet.

mattulbrich
authored and
wadoon
committed
correcting conversion in JML scripts

mattulbrich
authored and
wadoon
committed
adapting taclets.old.txt to changed throws treatment

mattulbrich
authored and
wadoon
committed
Repaired a merge test case

mattulbrich
authored and
wadoon
committed
missing sameUpdateLevel for tryCatchThrow

mattulbrich
authored and
wadoon
committed
spotless
wadoon
committed
fix regression fixtures taclets.old.txt
wadoon
committed
fix rebasing
wadoon
committed
fix tests
wadoon
committed
remove codecov
wadoon
committed
spotless
wadoon
committed
add converter
wadoon
committed
make userData type safe
wadoon
committed
spotless
wadoon
committed
fix SortDependingFunction uses
wadoon
committed
fix rebasing issue
wadoon
committed
update taclets.old.txt
wadoon
committed
fix proof
wadoon
committed
fix lexer
wadoon
committed
fix checkerframework
wadoon
committed
update proof
wadoon
committed
spotless
wadoon
committed
fix test case
wadoon
committed
fix wrong test fixtures
wadoon
committed

Commits on May 16, 2026

try to fix problems.
wadoon
committed