Repository navigation
Conversation
wadoon
changed the title
|
Phase 4 progress — slices 1–3 merged into this branch ( Phase 4 deletes
Slice 3 details: specs attach to the AST nodes they describe; visible Verification at the slice-3 HEAD (
Next: slice 4 = proof↔PO registry ( |
|
Phase 4 progress — slices 1–4 merged into this branch ( Phase 4 deletes
Slice 4 details: the proof↔PO bookkeeping moves verbatim out of Verification at the slice-4 HEAD (
Next: class invariants/axioms ( |
|
Phase 4 progress — slices 1–5 merged into this branch ( Phase 4 deletes
Slice 5 details: the invariant/class-axiom machinery moves verbatim out of Verification at the slice-5 HEAD (
Next: the contract registry ( |
|
Phase 4 progress — slices 1–6 merged into this branch ( Phase 4 deletes
Slice 6 details: the contract machinery moves verbatim out of Verification at the slice-6 HEAD (
Next: slice 7 — move the initially clauses ( |
|
Phase 4 progress — slices 1–7 merged into this branch ( Phase 4 deletes
Slice 7 details: the initially-clause machinery moves out of Verification at the slice-7 HEAD (
Next: slice 8 — collapse |
|
Phase 4 complete — Phase 4 deleted
Slice 9 details: the last remaining piece of the repository was the Verification at the Phase-4-completion HEAD (
Phase 4 is done; nothing remains in the plan table but ✅ rows. Possible |
wadoon
changed the title
|
CI triage after the Phase-4 slices (7–9) + spotless fix Fixed: Everything else that is red was already red before Phase 4 slices 7–9 —
The Phase-4 slice verification itself is unaffected: |
ca265f5 to
fd12879
Compare
Branch history rewritten — every commit is now spotless-cleanI reformatted the whole branch with
The slice table in the PR description has been updated to the rewritten commit CI checks re-ran automatically on the force-push; the only newly fixed job is |
f8a64c8 to
7cd8ec9
Compare
1afd808 to
048f75d
Compare
|
The current gap between JMLtk and KeY. Here are authentic examples for each entry, straight from the repo's fixtures, grouped by what JMLtk does with them. 1. Hard rejects — JMLtk has no grammar for theseComment-form //@ merge_point
//@ merge_proc "MergeByPredicateAbstraction"
//@ merge_params {conjunctive: (int x) -> {x >= 0, (x == \old(b) || x == -\old(b))}};JMLtk knows only the raw Java statement
/*@ assert x > 2 \by {
assert x == 7 \by { assume x == 7; auto; }
auto;
} */
@ public no_state static model \seq b(\bigint n) {
@ return n == 0 ? \seq_empty : \seq_concat(b(n-1), \seq(0));JMLtk: "In an embedded DL expression, Comma-separated //@ represents footprint = this.*, o.*;
//@ private represents footprint = array, array[*], size;Record-declaration-level /*@ nullable */ record MyRecord(String test) { ... }"Not JML construct supported" — only component-level (per-parameter)
/*@ spec_java_math @*/
public class Test { ... }JMLtk's KeY's label-after-assert form //@ assert LAB: e; // KeY's JmlParser.g4 assertion form
//@ LAB: assert e; // JML standard prefix form — the only one JMLtk accepts2. Silently mis-parses — worse than a clean errorAssignment /*@ public normal_behaviour
@ ensures \result = max;
@*/Previously KeY's own grammar rejected this with "Assignment operator '=' is not allowed in a JML specification expression" + position. JMLtk accepts it as an assignment expression, so KeY must now catch it structurally later (via Datagroup / monitor clauses — tokens absent → spurious declaration ( //@ monitors_for g; // silently mis-parses into a JmlFieldDeclaration("g")
//@ readable_if g; // same
//@ writable_if g; in_group g; maps_into g; datagroup g;3. Absent tokens (clean-ish reject), KeY's grammar had them//@ nowarn; // pragma-statement
//@ debug; // pragma-statement
//@ assignable \strictly_nothing; // no token; \nothing/\everything also become plain NameExpr
//@ captures o; // clause keyword absent
//@ requires ...; //@ when ...; // when / duration / working_space / spec_name all absent4. Parses fine, but semantics differ (proof-level follow-ons)
@ ensures \result == (\sum int i; 0 <= i && i < a.length; a[i]);JMLtk parses it, but Want these written into the branch as a standalone |
…Y's //@ merge_point form
- setProcessJml(true): JmlProcessor attaches JmlContract/JmlClassLevelDeclaration/ JmlExpressionStmt directly to the Java AST - setJmlKeys: map KeY's +KEY/-KEY/+OPENJML marker policy onto JMLtk key sets from GeneralSettings.getJmlEnabledKeys() - setKeepJmlDocs(true): transitional — legacy JMLTransformer still reads raw JmlDoc text; removed once JMLTransformer is gone (Phase 3)
Remove the ANTLR-based JML pre-parsing front-end and consume JMLtk's parsed AST (com.github.javaparser.ast.jml.*) directly, keeping KeY's specification translation semantics. Main changes: - New JmlSpec record wraps a JMLtk AST node (Node); KeY declarations, statement blocks and loops carry ImmutableList<JmlSpec>/List<JmlSpec> as attached JML (KEY_LOOP_SPEC deleted; merged getSpec on loops). - JMLTransformer rewritten: JMLtk already attaches parsed JML to the Java AST, so the transformer only relocates the nodes into the KEY_SPEC_CASE/KEY_CLASS_SPEC data keys, unwraps JmlMethodDeclaration/ JmlFieldDeclaration, and self-marks JML statements (assert/assume/set as JmlExpressionStmt, ghost vars, KeyMergePointStmt). - JMLSpecExtractor rewritten: dispatches JmlSpecs to the factory (class specs via node instanceof, method specs per-spec); keeps createNonNullPositionedString/arrayDepth. - JMLSpecFactory: new JmlSpec overloads for all entry points plus the implicit-clause enrichment (purity assignables, \inv requires/ ensures/signals, non-null pre/post, default signals-only, synthetic MODEL_BEHAVIOR for model methods) moved from the old extractor. - New JmlToTextual re-serializes JMLtk nodes against KeY's JML grammar (JmlParser.g4) rule by rule and hands the parse trees to the KeY-specific translation. - JP2KeYConverter: JmlExpressionStmt and KeyMergePointStmt are translated directly (re-parsed with the KeY grammar); loops use the merged spec list. - SpecialJavaPrinter prints JmlSpec nodes; JMLInfoExtractor returns ImmutableList<JmlSpec>. Known degradation (accepted): JMLtk has no statement-level merge support, so parametric merge (merge_proc/merge_params) only works via the KeY statement-level re-parse of the KeyMergePointStmt expression. Compiles: :key.core:compileJava GREEN.
…rded jmltk gaps, zero new regressions)
…of SpecificationRepository into new Services-owned ContractRegistry
Move the entire contract machinery out of de.uka.ilkd.key.proof.mgt.SpecificationRepository
into a new de.uka.ilkd.key.speclang.ContractRegistry (owned by Services, created via the new
Profile.createContractRegistry(Services) hook, shared by Services.copy like the spec repo /
proof registry / class-axiom computer):
- ContractRegistry holds the contract maps (contracts/operationContracts/contractsByName/
contractTargets per (KeYJavaType,IObserverFunction) node), the contract id counters,
initially clauses and the resolution helpers (getOverridingTargets/getInheritedContracts/
prepareContract/splitContract/combineOperationContracts/getContractByName/map).
- WdProfile now returns ContractRegistryWD (de.uka.ilkd.key.wd) which absorbs the WD hooks
from SpecificationRepositoryWD: wdChecks map, register/unregisterContract overrides,
registerWdCheck/unregisterWdCheck, getWdChecks/getAllWdChecks/getWdMethodChecks (now
package-private)/getWdClassChecks, WD getContracts/getAllContracts filter, map override,
addWdStatement, and package-private bridges for ClassAxiomComputerWD.
- CONTRACT_COMBINATION_MARKER ("§") moved to ContractFactory; references updated in
BlockContractImpl/LoopContractImpl/FunctionalAuxiliaryContract/ProofRegistry.
- Initially-clause machinery (createContractsFromInitiallyClauses/addInitiallyClause(s)) moves
into the registry in this slice; it leaves for JMLSpecFactory in a later slice.
- SpecificationRepository shrinks to a thin dispatcher: ctor, map (registry + class-axiom
computer), addSpecs (Contract/InitiallyClause -> registry; ClassInvariant/ClassAxiom ->
computer; loop/block/merge -> AST nodes) and the empty processJavaType hook.
SpecificationRepositoryWD keeps only the WD processJavaType override.
- TacletPOGenerator.generate now takes Services instead of SpecificationRepository (its only
impl WDTacletGenerator reads getAllWdChecks() from (ContractRegistryWD) services.getContractRegistry()).
- All callers rewired (load pipeline SLEnvInput/KeYFile, PO loaders, rules, replay, UI dialogs,
proofmanagement console checks, example main, test helpers); ProofRegistry splitContract/
getOverridingTargets/marker and ClassAxiomComputer.getOperationContracts delegation switched
to the registry.
Verified: :key.core(+wd/testgen/infflow/proofmanagement/ui/example):compileJava green;
speclang slice + IntSemanticsTest 285/0/12 (recorded slice-5 baseline); key.core.wd 1/0/0,
key.core.testgen 15/2/0, key.ui 44/1/0 all green. key.core.infflow:test has 3 pre-existing
InfFlowProfileLoadingTest failures (verified identical at Phase-3 HEAD d9ead21 and at
slice-5 HEAD — stale bracket-vs-paren contract naming in the example, unrelated to this slice).
No test code references deleted repository methods.
…rvices) in HANDOFF/PLAN - HANDOFF §1: HEAD has the first six Phase-4 slices; repo is now a thin dispatcher (map/addSpecs/empty processJavaType). - HANDOFF commits table + §7.3 step 3: slice 6 landed as 005320b, with the slice-6 verification record (speclang 285/0/12 + IntSemantics 6/0/0, key.core.wd 1/0/0, key.core.testgen 15/2/0, key.ui 44/1/0; the 3 InfFlowProfileLoadingTest failures pre-existing, A/B-verified at Phase-3 and slice-5 HEADs). NEXT = slice 7 (initially clauses → JMLSpecFactory load path). - PLAN §Phase 4: progress block now slices 1-6 DONE; contract-registry, combination/split, ids and inheritance table rows marked ✅ (moved to ContractRegistry / CONTRACT_COMBINATION_MARKER → ContractFactory); initially clauses row marked in-flight (registry this slice, JMLSpecFactory next).
…JMLSpecFactory load path Move the initially-clause machinery from de.uka.ilkd.key.speclang.ContractRegistry into the JMLSpecFactory, which is where the constructor-postcondition derivation belongs (its ContractFactory.cf already translated initially clauses via initiallyClauseToContract): - JMLSpecFactory gains the initiallyClauses per-type map plus addInitiallyClause/addInitiallyClauses (collection during loading) and createContractsFromInitiallyClauses()/createContractsFromInitiallyClause (derivation, called once after all contracts are registered; the derived constructor contracts are registered through services.getContractRegistry() via addContractNoInheritance/unregisterContract/cf.addPost/cf.func — the WD registry's registerContract override keeps creating the WD checks). - ContractRegistry drops the initiallyClauses field, addInitiallyClause(s), createContractsFromInitiallyClauses and the private derivation helper; its map(...) no longer maps initially clauses. unregisterContract becomes public so the factory can unregister replaced constructor contracts (WD subclass override bumped to public accordingly). - SpecificationRepository.addSpecs no longer dispatches InitiallyClause (the repo is Contract/ClassInvariant/ClassAxiom/loop/block/merge only now); the load pipeline (SLEnvInput.createSpecs, which already owns a JMLSpecFactory for the transform pass) partitions InitiallyClause out of the class specs, feeds them to the factory, and calls createContractsFromInitiallyClauses() at the end of loading — same position and ordering as before. Verified: :key.core(+wd/testgen/infflow/proofmanagement/ui/example) main+test compileJava green; speclang slice + IntSemanticsTest 285/0/12 (recorded baseline); key.core.testgen 15/2/0, key.core.wd 1/0/0, key.ui 44/1/0 all green; key.core.infflow 4/3 fail = the 3 pre-existing InfFlowProfileLoadingTest failures only (stale bracket-vs-paren contract naming in the example, verified pre-existing at Phase-3/slice-5 HEADs). One testgen run hit an environment OOM (exit 137, heavy concurrent load incl. the silent-wizard key.ui run); rerun solo passed. No test code references the removed methods.
… path) in HANDOFF/PLAN - HANDOFF §1: HEAD has the first seven Phase-4 slices; repo is still a thin dispatcher (map/addSpecs/empty processJavaType); NEXT = addSpecs collapse + map(...) removal. - HANDOFF commits table + §7.3 step 3: slice 7 landed as fd32802 with the slice-7 verification record (all main+test compile green incl. the one WD visibility-bump for the now-public unregisterContract; speclang+IntSemantics 285/0/12; module suites run solo after a combined run OOM'd (exit 137) — key.core.testgen 15/2/0, key.core.wd 1/0/0, key.ui 44/1/0; infflow 4/3 = the 3 pre-existing InfFlowProfileLoadingTest failures only). NEXT = slice 8 (addSpecs collapse + map removal), then repo deletion. - PLAN §Phase 4: progress block now slices 1-7 DONE; initially-clauses table row marked DONE (factory collects at load, derives constructor contracts at end of loading, same ordering).
… from the repo/registry/computer surface SpecificationRepository is now down to its constructor and the empty per-type processJavaType hook (the last slice deletes it together with the Services/ KeYEnvironment accessors, Profile.createSpecificationRepository, WdProfile override and SpecificationRepositoryWD): - SLEnvInput.createSpecs: the addSpecs dispatch collapses into a private registerSpecs helper (formerly SpecificationRepository.addSpecs) that routes each element verbatim: Contract → services.getContractRegistry().addContract, ClassInvariant/ClassAxiom → services.getClassAxiomComputer().add/invariants, LoopSpecification/BlockContract/LoopContract/MergeContract → their AST nodes. All three load sites (class specs, method specs, constructor specs) call it directly with initConfig.getServices() — same iteration order as before, so contract-id assignment is unchanged. - SpecificationRepository.map, ContractRegistry.map + the mapValueSets helper, ClassAxiomComputer.map + its mapValueSets helper, and the ContractRegistryWD map override (wdChecks remap) are deleted: the top-level walkers had zero callers anywhere in main or test code (the per-element SpecificationElement.map(UnaryOperator, Services) API itself stays — the WD WellDefinedness implementations still use it recursively). The load-time at-pre/WD transforms re-walk the AST-attached specs instead of the global snapshot. - ContractRegistry thread-safety comment updated: maps are populated during problem loading and only read afterwards — no state is mutated during proving anymore (the synchronized-map rationale is gone with map(...)). Verified: :key.core(+wd/testgen/infflow/proofmanagement/ui/example) main+test compileJava green; speclang slice + IntSemanticsTest 285/0/12 (recorded baseline); module suites solo: key.core.testgen 15/2/0, key.core.wd 1/0/0, key.ui 44/1/0 green; key.core.infflow 4/3 = only the 3 pre-existing InfFlowProfileLoadingTest failures. Regenerated test fixture TestGeneric0.java restored after the testgen run. No test code references the removed methods.
The last remaining piece of SpecificationRepository, the per-type processJavaType hook, moves into the Services-owned contract registry, and the repository plus its accessors are deleted: - ContractRegistry gains an empty processJavaType(KeYJavaType) hook (the profile-created home for per-type post-processing, like the repository was); ContractRegistryWD overrides it with the body formerly in SpecificationRepositoryWD (RepresentsAxiom -> MethodWellDefinedness / addRepresents processing; the cast to ContractRegistryWD collapses to this). - SLEnvInput.createSpecs calls contractRegistry.processJavaType(kjt) instead of specRepos.processJavaType(kjt); the specRepos variable and the SpecificationRepository import are gone. - Deleted: SpecificationRepository.java and SpecificationRepositoryWD.java (key.core.wd), Service.specRepos field + getSpecificationRepository() + copy paths, KeYEnvironment.getSpecificationRepository(), Profile.createSpecificationRepository (default) + WdProfile override, and the SpecificationRepository imports in Services/KeYEnvironment/Profile/ WdProfile/ContractFactory (ContractFactory/ProofRegistry javadoc mentions downgraded to plain-text so no dangling @link remains). Phase 4 complete: the repository is gone; all specifications live on the AST nodes or in the Services-owned components (ContractRegistry, ClassAxiomComputer, ProofRegistry, JMLSpecFactory). Verified: :key.core(+wd/testgen/infflow/proofmanagement/ui/example) main+test compileJava green; speclang slice + IntSemanticsTest 285/0/12 (recorded baseline); module suites solo: key.core.testgen 15/2/0, key.core.wd 1/0/0, key.ui 44/1/0 green; key.core.infflow 4/3 = only the 3 pre-existing InfFlowProfileLoadingTest failures. Regenerated test fixture TestGeneric0.java restored after the testgen run. No test or main code references the deleted class or its methods.
…moval, SpecificationRepository deleted) in HANDOFF/PLAN Phase 4 is finished: SpecificationRepository.java no longer exists. - HANDOFF §1: HEAD contains all nine Phase-4 slices; SpecificationRepository is DELETED (e50d64b); specs live on the AST or in the Services-owned ContractRegistry/ClassAxiomComputer/ProofRegistry/JMLSpecFactory. - HANDOFF commits table + §7.3: slices 8 (2ae5b95: addSpecs collapse into SLEnvInput.registerSpecs + map(...)/mapValueSets removal from the repo/registry/computer surface; repo shrinks to ctor + processJavaType) and 9 (e50d64b: repo + Services/KeYEnvironment accessors + Profile.createSpecificationRepository + WdProfile override + SpecificationRepositoryWD deleted; processJavaType -> ContractRegistry/WD) with their verification records (speclang+IntSemantics 285/0/12, module suites solo, infflow 4/3 = the 3 pre-existing failures). §7.4 notes no Phase-4 work remains. - PLAN §Phase 4: progress block now says Phase 4 COMPLETE (slices 1-9); the map/addSpecs/thread-safety table rows marked DONE; the deliverable note marked REACHED; the ProofRegistry row's historical 'like specRepos' wording fixed.
…maining red jobs verified pre-existing (caching/slicing/infflow/integration proofs unchanged since slice-3-era commits)
…per-commit) weigl/jmltk-jml was rewritten with scripts/format_branch_with_spotless.sh: tree-filter 'gradle --parallel spotlessApply && git clean -ffdx' plus a commit-filter dropping the now-redundant 'spotless: fix formatting' fix-up commit (34 -> 33 commits). Every commit is spotless-clean, the final tree is identical to the pre-rewrite tree, and base 44ad23c is intact. Update HANDOFF/PLAN commit references to the rewritten SHAs and reword the CI-formatting notes (formatting fold, no e17111e).
JMLtk 1.1.0-SNAPSHOT no longer ships the KeY-specific getAssociatedSpecificationComments()/attachedJml carrier. Read the parsed JML specifications directly from the typed JMLtk AST instead: - Java AST classes: remove the attachedJml carrier and getAssociatedSpecificationComments(); createComments now returns Collections.emptyList(). - KeYJPMapping.registerReverse: register reverse (KeY -> JMLtk) mappings for classes (JmlTypeDeclaration) and callables (contract carrier). - JP2KeYConverter: keep the contract carrier for each KeY method via the reverse mapping; skip pure class-level JML constructs (invariant, initially, axiom, represents, accessible) when converting members. - JMLSpecExtractor: rewritten to read contracts, model method definitions, class-level specs and loop invariants from the JMLtk AST via the mapping. - JmlToTextual/JMLSpecFactory: overloads building spec texts from the typed classes (JmlContract, JmlMethodDeclaration, ...) and direct conversion of JmlContract/JmlMethodDefinition. - JMLTransformer: unwrap JmlMethodDeclaration/JmlFieldDeclaration wrappers into the member list again, since Javaparser symbol resolution ignores wrapped declarations; the wrapper is remembered on the inner node via the new KEY_JML_WRAPPER data key and is used as the contract carrier (model method definition, ghost field). - Delete JmlSpec.java.
…front-end The rebase onto jmltk 1.1.0-SNAPSHOT replaced the intermediate JmlSpec carrier/attachedJml design with a carrier-free one: KeYJPMapping reverse mappings are the only bridge between the ASTs and JMLSpecExtractor reads contracts, model method definitions, class-level specs, and loop/block contracts back from the JMLtk typed AST. - PLAN.md: final status header; §2/§2.2 pipeline diagram and §4 rewritten to the shipped architecture; Phase 0/1/2 marked DONE/SUPERSEDED; §7 Q1-2 resolved; §8 replaced by the final build status. - JML_MAPPING.md: header + Part A (producers/carriers/consumers) rewritten to the shipped design; Part E updated (no carrier between the ASTs). - HANDOFF.md: header + §1 mark the completion (HEAD d2b2112, 279/0/12 speclang slice, whole-build compile + spotless green); §2 rewritten to the final front-end; §3 model-method detection updated; §7 resume list closed.
Close the paths in the JMLtk-based JML front-end where a construct that
JMLtk accepts could be silently dropped, weakened, or mis-translated on
its way through KeY's own JML grammar and term translation.
- JmlToTextual: hard-fail on untranslatable clauses instead of
catch-and-skip. The KNOWN_GAPS allow-list starts empty; a clause is
only skippable after its loss is triaged as acceptable. Unknown class
level construct kinds are rejected loudly instead of skipped. The
JmlSideEffectChecker runs on every translated contract and clause.
- JmlSideEffectChecker: new structural AST guard (not a text scan) that
rejects assignment operators, ++/--, object creation, and array
creation inside JML specification expressions. set statements and
ghost declarators are exempt (assignment is their point), and the
visitor never descends into Java bodies. Wired into JmlToTextual
(contracts, loop specs, class level clauses) and the assert/assume
branch of JP2KeYConverter.
- JMLTransformer: class level "field-like" clauses that JMLtk models as
JmlFieldDeclaration with a bogus type (the keyword) can no longer
become spurious Java fields. The datagroup family (datagroup,
in_group, maps_into, monitors_for, readable_if, writable_if,
mapped_by, repr) is rejected loudly; captures/duration/working_space
remain accepted drops of deprecated legacy clauses.
- JmlDocRemoval: a `name "..."` clause that JMLtk cannot parse would
silently drop the whole spec case containing it; such leftover JmlDoc
nodes are now rejected loudly (word-boundary guarded so `spec_name`
clauses stay accepted drops).
- JmlToTextual serializers: signals clauses omit the binder name
(`\exception`) that JMLtk synthesizes; the information-flow
serializer is rewritten to JMLtk's shifted getters (getBy ->
getDeclassifies -> getErases -> getExpressions -> getNewObjects),
emits the terminating `;`, wires loop_determines/loop_separates to
KeY's loop clause grammar, and rejects a \declassifies/\erases
section that the loop clause grammar cannot express.
- Parallel-prover merge-contract safety: synchronized contract
accessors on StatementBlock/LoopStatement/MergePointStatement and a
new atomic MergePointStatement.setMergeContracts; ProgVarReplaceVisitor
and IntroAtPreDefsOp use it instead of the racy removeMergeContracts()
+ addMergeContract() sequence so concurrent rule application never
observes an empty contract set.
- Assertion proof scripts (`assert e \by { ... }`): JP2KeYConverter
re-parses the JMLtk JmlProofStmt list against KeY's assertionProof
grammar into KeyAst.JMLProofScript instead of dropping the script; a
script JMLtk accepted but KeY cannot re-parse fails loudly. Applies
to assert and assume (new AssertionProofScriptTest).
- Quantifier round-trip fixtures: SumClause and BsumClause lock that
\sum and \bsum (canonical `(\bsum T v; from; to; summand)` range
form) survive the JMLtk -> KeY re-parse verbatim; \bsum keeps its
loud deprecation warning in JmlTermFactory.
- Spec math modes: restore the class level spec_*_math pragmas in the
specMath fixtures (JMLtk parses them as real JML modifiers), re-enable
specMathJavaMathTest/specMathBigintMathTest in ContractLoadingTests,
and add SpecMathModeTest covering class, method, and inline
model-method modes.
- JMLtk snapshot pin: build.gradle comment documents why the 1.1.0-
SNAPSHOT snapshot repository is kept (release 1.0.0 lacks the
ast.jml.proof package) and tracks jmltoolkit/jmltk#82 for pinning.
New exceptional-fixture guards (JMLParserExceptionTest): WrongEquals is
now a loud JmlSideEffectException (assignment in an ensures clause),
plus IncrementInContract, ObjectCreationInContract, NoSideEffects,
Datagroup, DeprecatedDrops, NameClause, and NameClauseClass.
JMLtk's grammar cannot parse KeY extension statements inside //@ comments (merge point statements, set statements, and assert/assume statements with KeY proof scripts or obtain clauses). Instead of dropping them, re-parse the leftover comment with KeY's own JmlParser, mark the JmlDocStmt with the parsed methodlevel_element (KEY_JML_FALLBACK), and translate it in the converter. - JMLTransformer: re-parses unhandled method level JML comments and attaches the parse tree to the leftover JmlDocStmt. - JavaService.unwrapParseResult: tolerates the JMLtk gap problems and re-injects the symbol resolver when the tolerated problems suppressed it. - JP2KeYConverter.visit(JmlDocStmt): translates merge points, set statements and asserts/assumes (incl. KeY proof scripts) from the fallback parse tree. - JMLSpecExtractor/JMLSpecFactory: derive merge contracts from the fallback parse tree. Also fixes two regressions of the JMLtk front-end: - visit(KeyMergePointStmt): keep the MergePointStatement wrapper in the schema (taclet pattern) branch, so deleteMergePoint matches again and automatic merge proving/stored-proof replay work. - handleSpecialFunctionInvocation: translate \seq(...) sequence literals by concatenating singleton sequences, mirroring TermBuilder.seq. Previously embedded \seq(...) in model method bodies was rejected as an unknown DL function (Issue3452Test failed).
The rebase onto main brings the merged type-annotations feature, which changed the TypeReference API of TermBuilder (selfVar takes TypeRef now) and the TypeDeclaration constructor surface. Adapt the JML front-end takeover to it: - AnnotationInterfaceDeclaration: drop the removed TextualJMLConstruct jmlAttachments parameter (branch deleted the carrier in Phase 1) - JP2KeYConverter.visit(AnnotationDeclaration): no longer pass getClassSpec - ClassAxiomComputer: selfVar(kjt) -> selfVar(new TypeRef(kjt), ...)
…ed/changed under JMLtk Records every JML construct/test that worked with KeY's pre-takeover front-end but is rejected, silently mis-parsed, or behaviorally different under the JMLtk front-end, with authentic fixture snippets, fixture paths, and per-entry status measured at HEAD. Notable measured findings at 048f75d: - comment-form merge_point, \by proof scripts, \seq escape and proof-starter cases are RESOLVED by the KEY_JML_FALLBACK re-parse mechanism - \seq is corrected: the old 'not a known DL function name' failure is a KeY name-resolution issue (JP2KeYConverter), not a JMLtk parse rejection - KeyJavaPipelineTest is an uncovered REGRESSION: 86/136 red (0 on main), not part of the recorded 34-failure baseline - remaining open gaps: comma-separated represents loads, \sum proofs, labeled-break proof, relax.proof replay, records pipeline, spec_*_math, and the absent clause/pragma/datagroup tokens
…refix Named spec cases are written as `[behavior] <name>:` (an identifier prefix, e.g. `public normal_behavior CaseA: ...`), the only form JMLtk parses into JmlContract.name. JmlToTextual.toSpecCase already maps it via addName to the spec-case name and JMLSpecFactory.generateName to the operation contract base name, so no translation change is needed - only the source form and the guard fixtures. - JmlDocRemoval: the legacy `name "..."` clause stays a loud error (JMLtk cannot parse it and it would silently drop the whole spec case), but the message now points to the replacement `[behavior] <name>:` prefix form. - NameClause (exceptional, prev. expected ProofInputException 'Case A'): becomes the positive fixture testcase/speclang/njml/NameClause.java using the new form; ContractLoadingTests.nameClauseCarriesContractName asserts the operation contract base name is 'CaseA'. - NameClauseClass (class level legacy `name "..."`): still a loud error; comment documents that class-level spec naming has no JMLtk counterpart. - JMLTK_GAPS.md row 12: `name` is replaced (RESOLVED), not lost.
The record goldens were generated by the old PreParser-based attachSpec and
no longer matched the current pipeline output. With the JMLtk front-end the
generated specs are printed faithfully, so the goldens are regenerated from
the branch's fresh 'actual/' output (102 -> 108 files, 136 -> 142 tests).
Semantic differences in the generated code/specs:
- hashCode() == o.hashCode() ==> !\result -> hashCode() != o.hashCode() ==> !\result
and 'o == null ==> !\result' -> 'o != null ==> !\result' (stages 05-16, 18):
the old forms came from the PreParser's re-serialization; JMLtk prints the
RecordClassBuilder template (which already used '!='/ '!=') truthfully.
- removed '[[JML modifiers]]' placeholder markers in early stages (01-06);
JMLtk records real modifiers instead.
- nullable annotations are kept inline ('/*@ nullable */') instead of being
detached into leading comments (01-06).
- new stage 17_AnnotationMover with 6 golden files (the stage exists on the
branch but had no goldens yet).
The test is byte-exact: expected/ is identical to a fresh actual/ run
(108/108), KeyJavaPipelineTest is green (142/0).
… HEAD - HANDOFF §5.2 UPDATE block: rows (a) merge family, (b) JmlScriptTest, (c) Issue3452Test, (f) TestProofStarter are green at HEAD (measured 2161/0); row (j) KeyJavaPipelineTest re-measured as 86 failures (stale record goldens), now green 142/0 after the regenerated goldens; points to JMLTK_GAPS.md as the living record. Remaining open: 12 (rows d/e/g/h/i). - JMLTK_GAPS §6: status flipped from REGRESSION to RESOLVED — record goldens deliberately regenerated (expected 102 -> 108 files incl. 17_AnnotationMover), KeyJavaPipelineTest 142/0, byte-exact vs fresh actual.
…al fixtures - JMLParserExceptionTest fixtures: NowarnDebug (class-level loud ProofInputException) and NowarnDebugInMethod (method-level drop via the JmlDocStmt fallback) pin the JMLtk-absent pragma-statements. - MonitorsFor/ReadableIf/WritableIf/InGroup/MapsInto lock the JMLTransformer DATAGROUP_FAMILY guard per keyword: loud IllegalArgumentException, no spurious fields. - JMLTK_GAPS.md §13/§14 + status table, JML_MAPPING.md gaps 4-5 and PLAN.md item 5 updated to the measured state at this commit.
655b99e to
8fe1be5
Compare
- Re-ran the Appendix A suite at 8fe1be5 (192 tests, 12 failed) and re-confirmed every recorded count: merge family 12/12 (+3 PredicateAbstractionLatticeTests), JmlScriptTest 7/7, Issue3452Test 2/2, ScDeterminismTest 4 load + 3 proof failures, RealProofMtEquivalenceTest 1, KeyJavaPipelineTest 142/0, LoopScopeInvRuleTests 1, 2 replayer failures, ParallelProverDeterminismTest 1 (flags have to have the same size). - Header now records measurement at the rebased tip 8fe1be5 (Nov 2 2026). - Remap rewritten commit hashes: 048f75d->bf7048ca5d, edbed71-> 251f945, 10f4bfc->841b999eee. - Fixture path corrections: arrayMax.key and polishFlagSort.key live under standard_key/java_dl (not heap/comprehensions respectively heap/); exact heap/{list,simple} prefixes for the four ScDeterminismTest load files.
The doc still recorded the pre-remediation state (pragmas removed, two load tests @disabled). At 8fe1be5 the fixtures carry their spec_java_math/ spec_bigint_math pragmas again and the R4 mapping via ModifierKind.JML_SPEC_* to SpecMathMode is in place: SpecMathModeTest (2) and ContractLoadingTests (6, incl. specMathJavaMathTest/specMathBigintMathTest) are green.
…loop nodes
The loop-invariant taclets (loopScopeInvDia & co.) bind #loopStmt via
\storeStmtIn, which instantiates the taclet's pattern template
'while (#nse) #body' and thus yields a *fresh* LoopStatement (position
UNDEFINED) that is only structurally equal to the loop in the goal. The
pre-JMLtk SpecificationRepository resolved specs by structural (loop,
line) key, so the fresh node still found its invariant; the node-attached
loopInvariant field is null on the fresh node and the rules failed to
match ('rule loopScopeInvDia not available or not applicable'), breaking
replay of any saved proof applying a loop-invariant rule (e.g.
reverseArray.proof node 90).
Add LoopStatement.getLoopInvariant(Statement program): when the node
itself carries no invariant, search the given program for a structurally
equal loop that does (mirroring the old map semantics) and use it. Apply
the fallback in the four loop varcond classes (hasInvariant,
getInvariant, getFreeInvariant, getVariant) and in
MiscTools.getSpecForTermWithLoopStmt (CreateHeapAnonUpdate,
CreateFrameCond), which suffered the same regression on the stored
loopFormula term.
Three independent drifts between the JMLtk front-end and the retired
PreParser/TextualJML front-end changed the loaded KeY program or its
specifications enough to break replay of saved proofs (and, with it, the
slicing and caching suites that load and re-prove stored proofs).
1. Model/ghost methods (JP2KeYConverter). A method unwrapped from a
JmlMethodDeclaration carried its JML definition as an executable body,
so e.g. `\old`-containing model-method text was built as Java code
("In an embedded DL expression, \old is not a known DL function
name."). The pre-JMLtk front-end produced signature-only KeY methods
for these (TextualJMLMethodDecl.getParsableDeclaration emits `...;`);
the definition is a specification, translated via the JML grammar
(JmlToTextual.toMethodDecl, AXIOMS). Convert the body as empty when a
JML wrapper is present.
2. Model-method contracts (JMLSpecExtractor). JMLtk attaches the contract
to the inner MethodDeclaration (a NodeWithContracts), while
JmlMethodDeclaration.getContract() is empty for them; the extractor
only read the wrapper, so the contract was lost and the fallback built
a trivial `true` contract, leaving the model method without a
`requires`/`ensures` axiom (replay then fails on
`Contract_axiom_for_..._in_...`). Collect from both carriers.
3. JML field initializers (JMLTransformer). JMLtk keeps a JML field
declaration's initializer on the wrapped FieldDeclaration; the
pre-JMLtk front-end materialized class-level JML fields without
initializers, so they never reached the constructors. The kept
initializer (e.g. `//@ ghost ... = null` in java.lang.Throwable) was
inlined into the synthetic `$init`, changing the method body and
breaking `methodCallEmpty` in stored proofs. Strip initializers when
unwrapping JmlFieldDeclaration.
Verified: keyext.slicing 23/23 green (sliceJavaProof,
sliceMultipleIterations, Issue3834Test, IssueRenamingTest,
ProofListenerIsolationTest).
JMLtk 1.2.1 parses the comment-form merge point (`//@ merge_point ...`)
into a new typed statement node `JmlMergePointStmt`
(`com.github.javaparser.ast.jml.stmt`, added in this release) instead of
leaving it as an unparsed leftover comment. The converter had no handler
for it, so the default visitor walked the node's children and aborted on
the JML key tag `SimpleName` ("Unsupported element detected ...
SimpleName"), breaking the load of every proof with a merge point
(MergeRuleTests 9x "Load failed"). A/B-confirmed: green at 1.1.0, red at
1.2.1, otherwise identical code.
- JP2KeYConverter: visit(JmlMergePointStmt) -> a MergePointStatement
holding a temporary boolean location variable, mirroring the re-parsed
fallback form (the node carries no executable expression).
- JMLSpecExtractor: route a mapped JmlMergePointStmt to the merge-contract
factory.
- JMLSpecFactory: new createJMLMergeContracts overload that re-serializes
the node's optional merge procedure / lattice / predicate metadata to the
textual `merge_point` statement and re-parses it with KeY's JML grammar,
reusing the shared translation (so proc and merge_params are honored).
Verified under 1.2.1-SNAPSHOT: MergeRuleTests 12/12,
PredicateAbstractionLatticeTests 3/3; key.core recorded-baseline re-run
shows no new failures.
JMLTK_GAPS.md: - Re-measured at 53dcefd (jmltk 1.2.1-SNAPSHOT + the typed merge-point handler): key.core red count is 11 (was 14); the loop-invariant structural-lookup fix (6a07c20) resolved 3 recorded reds. - S5: arrayMax.key/polishFlagSort.key were loop-invariant regressions, not \sum-fidelity failures — corrected and removed from the gap. - S9: marked RESOLVED with the root cause. - S10: extended with keyext.caching TestReferenceSearcher and the node-40 root cause (assignable \strictly_nothing postcondition frame). - S1: recorded the 1.2.1 typed JmlMergePointStmt handling (53dcefd). - New S17: [no file] in origin term labels — cosmetic only (labels are proof-irrelevant), documented, not fixed. TODO_CI.md: the CI red-hunt record for PR #3997 — the four stored-proof replay root causes behind the 5 keyext.slicing failures, the keyext.caching triage (1 fixed, 1 accounted under the recorded relax.proof gap), the jmltk 1.1.0 -> 1.2.1-SNAPSHOT bump with A/B evidence, and the final per-job state at the branch tip.
The 2026-11-08 CI run at 4b62b1d triages the remaining red integration jobs: - testRunAllWdProofs is now green (was red at 2026-11-02) - resolved by the program/spec-shape fixes. - testMt2w/testMt4w: the curated small-MT collections contain exactly the recorded store-ref/sum failures (S4/S5); no new MT prover failure. - testMtStress: MtScriptStressTest x2 fail to LOAD heap/quicksort/sort.key - newly identified, pre-existing (identical failure in the 2026-11-02 CI at 1.1.0-SNAPSHOT), previously unrecorded because the testMt*/testRunAll* jobs were not part of the local baseline. Root cause: JMLtk (both 1.1.0 and 1.2.1) parses the KeY-specific ghost local '//@ ghost \seq x = \dl_array2seq(a);' as a class-level JmlFieldDeclaration and reports a hard problem that JavaService.unwrapParseResult does not tolerate. Recorded as S18 with fix options. - TODO_CI S4 updated with the per-job triage state.
…locker Local corpus runs of testRunAllFunProofs (22 red groups) and testRunAllInfProofs (10 red groups) at the branch tip complete the integration triage. origin/main's Tests workflow is fully green, so every Fun/Inf red is PR-induced (the front-end swap); the Fun set shrank 33 -> 22 between the 1.1.0 and 1.2.1 CI runs via the program/spec-shape fixes. New gap families recorded in JMLTK_GAPS.md: - S19: JMLtk accepts the standard-JML 'ensures_redundantly' clause but KeY's JmlParser.g4 has no production for it, so JmlToTextual throws 'Unsupported clause kind' and the whole source fails to load (SmansEtAl group). - S20: the 'assignable_free <expr>' clause makes the converter run the symbol resolver on the clause keyword, an UnsolvedSymbolException aborts the load (javadl group). - S21: the tracked heap/permutedSum/perm.proof still loads but its recorded replay now has 6 errors (stored rule position no longer fits the sequent, One Step Simplification not reconstructable) - a stale recording against the new front-end, same family as the relax.proof gap (S21). S17 upgraded from cosmetic to a save->reload blocker: saved proofs carry 'requires @ [no file]' origin strings that OriginTermLabelFactory.parseOrigin rejects (renderer/parser asymmetry), so reload-enabled RunAll groups (other, list_seq) fail; fix options recorded. S4 extended with the RunAll corpus fixtures it breaks (list, javaCard, funOfIF, simple_info_flow, simpleTests, Inf NewObjects).
Intended change
Rewrite how KeY handles JML specifications: remove KeY's own hand-written ANTLR JML front-end and the entire
TextualJMLConstructpre-parsing machinery (plusSpecificationRepository), and consume JMLtk's parsed JML AST (ast.jml:JmlContract,JmlClause,JmlClassLevelDeclaration, …) directly as the single source of truth. KeY keeps its specification semantics: theJMLSpecFactorytranslation (JML terms → JavaDL terms/speclang objects) remains, withJmlToTextualre-serializing each JMLtk clause/declaration against KeY's ownJmlParser.g4rules so the provenTranslator/JmlTermFactorymachinery is reused unchanged.Status / progress
PLAN.md) and the construct-mapping/gap list (JML_MAPPING.md)JavaParserFactory(setProcessJml(true), JML-keys policy)JmlSpecwrapper, noattachedJmlfields, no data-key spec relocation:JMLTransformerunwrapsJmlMethodDeclaration/JmlFieldDeclarationwrappers back into the member list (Javaparser's symbol resolution ignores wrapped declarations) and remembers the wrapper on the inner node via the newKEY_JML_WRAPPERdata key; it self-marks the JML statements (JmlExpressionStmt→KEY_ASSERT/KEY_ASSIGN,KeyMergePointStmt→KEY_MERGE_POINT, ghost variables →JML_GHOST).JP2KeYConverterconverts the Java declarations, skipping the pure class-level JML constructs (invariant, initially, axiom, represents, accessible — they stay on the JMLtk type), registers the KeY→JMLtk reverse mappings viaKeYJPMapping.registerReverse(TypeDeclaration→JmlTypeDeclaration, each method/constructor → its contract carrier), translatesJmlExpressionStmt→JmlAssert/SetStatementandKeyMergePointStmt→MergePointStatement, andcreateCommentsreturnsemptyList()(the parsed JML is not carried as comments anymore).JMLSpecExtractoris rewritten to read the specs back from the JMLtk AST viaKeYJPMapping.nodeFromKeY: method contracts and model-method definitions from the contract carrier, class-level specs from the JMLtk type members, loop invariants by scanning theJmlContracts on loop statements, block/loop/merge contracts from the attached contracts.JMLSpecFactorygained direct-class overloads (createJMLOperationContracts(pm, JmlContract, ParserRuleContext modelMethodDefinition, boolean addInvariant),createJMLModelMethodContracts(...)), and the implicit-clause enrichment (purity assignables,\invin requires/ensures/signals, non-null pre-/postconditions, default signals-only, syntheticMODEL_BEHAVIORfor model methods) moved there unchanged from the old extractor.JmlSpec.java, theattachedJmlcarrier andgetAssociatedSpecificationComments(), theKEY_SPEC_CASE/KEY_CLASS_SPECrelocation,PreParser/TextualTranslatorand theTextualJML*intermediate layer.JmlToTextualre-parse bridge as the semantics layer: JML grammars andTranslator/JmlTermFactory/JmlIO/JmlFacadestay; only the dead pre-parsing code is deleted.speclang.*slice is the parity contract and is green.SpecificationRepositorydeleted, in nine slices (specs stay attached to the AST / owned byServicescomponents; no global snapshot): slice 1 statement specs onJmlAssert/SetStatement(e222eb6b33), slice 2 limited observers (51c9a62dd7), slice 3 loop/block/merge specs on the statement nodes (63a536393b), slice 4 proof↔PO registry →ProofRegistry(b80363992a), slice 5 class invariants/axioms →ClassAxiomComputer(7495f9d167), slice 6 contract registry →ContractRegistry(ffc9fb9fd3), slice 7 initially clauses →JMLSpecFactoryload path (3300c2e0c3), slice 8addSpecscollapse +map(...)removal (4ca11a7e6d), slice 9SpecificationRepository.javadeleted (a962f66124).origin/main(which contains the JMLtk Java-parser migration Migrate to JMLtk #3966, merged as8bd51f0e59) and the final carrier-free front-end;jmltkstays pinned to1.1.0-SNAPSHOT.Latest updates (2026-10-30, pushed)
JMLTK_GAPS.md— new living status record of JML that worked before the takeover and its state under JMLtk (one entry per construct with re-verifiable fixtures, statuses measured atbf7048ca5d); supersedes the historicalHANDOFF.md§5.2 triage in both directions (f830558081).name "..."clause cannot be parsed by JMLtk (it would silently drop the whole spec case). Named spec cases are now written in the JMLtk-native[behavior] <name>:prefix form (e.g.public normal_behavior CaseA: ...), which JMLtk parses intoJmlContract.name;JmlToTextual.toSpecCasemaps it to the spec-case name andJMLSpecFactory.generateNameto the operation contract base name (consumer side already existed).JmlDocRemovalrejects the legacy string form loudly with a migration hint; class-level spec naming has no JMLtk counterpart (NameClauseClassstays a guarded failure). New positive fixture + testContractLoadingTests.nameClauseCarriesContractName(a7a39edaa5).PreParser-basedattachSpecand no longer matched the JMLtk front-end output (==/o == nullre-serializations,[[JML modifiers]]marker placeholders, detached nullable comments, missing17_AnnotationMoverstage).expected/was deliberately promoted from a freshactual/run (102 → 108 files);KeyJavaPipelineTestis green 142/0, byte-exact against a fresh run (841b999eee).HANDOFF.md§5.2 correction block andJMLTK_GAPS.md§6 status flip to resolved; the four now-green triage rows (merge family,JmlScriptTest,Issue3452Testincl. the\seqmis-attribution,TestProofStarter) were re-verified at HEAD (a8f86ee351).Latest updates (2026-11-02, pushed)
jmltksnapshot refreshed and re-verified — the PR is re-verified against the freshly published1.1.0-SNAPSHOT(2026-11-02;jmlparser-core,jmlparser-core-serialization,jmlparser-symbol-solver-coreresolve from the Sonatype snapshots repository).:key.corecompileJava/compileTestJavaand thede.uka.ilkd.key.speclang.njml.*slice re-run on the rebased tip.JMLParserExceptionTestcases inexceptional/:NowarnDebug(class level) andNowarnDebugInMethod(method level) pin the level-dependent behavior of the//@ nowarn;///@ debug;pragma-statements: class level raises a loudProofInputException("Encountered unexpected token"); method level falls back to KeY's own grammar and the leftover is dropped (JMLTK_GAPS.md§13).MonitorsFor/ReadableIf/WritableIf/InGroup/MapsIntolock theJMLTransformerDATAGROUP_FAMILYguard per keyword: loudIllegalArgumentException, no spurious fields (JMLTK_GAPS.md§14 → resolved).JMLTK_GAPS.md§13/§14 + status table,JML_MAPPING.mdgaps 4–5 andPLAN.mditem 5 updated to the measured state.JMLTK_GAPS.mdre-verified at the rebased tip — the full Appendix A suite (re)ran at8fe1be5b6c(192 tests, 12 failed) and every recorded count confirms: merge family 12/12 (+PredicateAbstractionLatticeTests3/3),JmlScriptTest7/7,Issue3452Test2/2,ScDeterminismTest4 load + 3 proof failures,RealProofMtEquivalenceTest1 (sum0),KeyJavaPipelineTest142/0 (108 golden files / 18 stages, incl.17_AnnotationMover),LoopScopeInvRuleTests1, 2 replayer failures,ParallelProverDeterminismTest1 ("flags have to have the same size"). Rebased-hash references remapped (048f75d7df→bf7048ca5d,edbed7177c→251f945131,10f4bfcb9a→841b999eee); fixture paths corrected (arrayMax/polishFlagSortlive instandard_key/java_dl/, notheap/). §7spec_*_mathflipped OPEN → RESOLVED: the R4 modifier→SpecMathModemapping is live at the tip withSpecMathModeTest(2) andContractLoadingTests(6, incl.specMathJavaMathTest/specMathBigintMathTest) green. Pushed asf127079310,ed348636cb.JMLParserExceptionTestcases (MethodInMethod,ModelFieldinMethod— amodeldeclaration inside a method body) fail identically under the previous and the refreshed snapshot (A/B-verified byte-identical JMLtk parse). This is a KeY-side leftover-JML fallback gap, tracked separately from the recordedJMLTK_GAPS.mdbaseline.Latest updates (2026-11-08, pushed)
TODO_CI.md). The red jobs of the 2026-11-02 CI run (key.core 14, keyext.slicing 5, keyext.caching 2) are now:keyext.slicing: 5 red → fixed, 17/17 green. All five were stored-proof replay failures: the JMLtk front-end produced a KeY program/spec that drifted from the pre-takeover front-end, so proofs recorded with the old front-end no longer matched at replay. Four root causes, two commits:6a07c20e63— theloopScopeInvDiafamily binds a fresh structurally-equalLoopStatement(position UNDEFINED) via\storeStmtInwhose node-attached invariant is null → structural reverse lookupLoopStatement.getLoopInvariant(program)(fixes theEndToEndTestsslicing replays andLoopScopeInvRuleTests).233ec1d9b0— (a) JMLtk attaches model-method contracts to the innerMethodDeclaration, not theJmlMethodDeclarationwrapper; the extractor only read the wrapper → trivialtruecontract and missingContract_axiom_*taclet → now collected from both; (b) JML model-method bodies were built as executable Java bodies (\old→ "not a known DL function name") → signature-only conversion when a JML wrapper is present (mirrorsTextualJMLMethodDecl.getParsableDeclaration); (c) JMLtk kept//@ ghost … = nullinitializers on unwrapped fields, inlined intoThrowable.$init→ stripped inJMLTransformer(the old front-end materialized JML fields bare).keyext.caching: 2 red → 1 fixed, 1 accounted.ProofCachingSingleRunTestis fixed by the loop-invariant fix (BinarySearch_search.keyproves aloop_invariant+decreasesloop);TestReferenceSearcherloadsrelax.proof— the same recorded OPEN gap as the two key.core replayers (JMLTK_GAPS.md§10; the replay succeeds but leaves theNull Referencecase open whose postcondition frame derives fromassignable \strictly_nothing, cf. gap <deleted> #15).key.core: 14 → 11 red, all recorded, no new. The loop-invariant fix additionally resolved 3 recorded reds (LoopScopeInvRuleTests,arrayMax.key,polishFlagSort.key— all loop proofs;arrayMax/polishFlagSortwere mis-attributed to\sum).KeyJavaPipelineTest142/0 — the program-shape fixes do not change the pipeline goldens.testMt2w/testMt4w/testMtStress,testRunAll*Proofs) — triage complete (see the next bullet):testRunAllWdProofsis now green (was red on 2026-11-02);testMt2w/testMt4w= the recorded §4/§5 gaps surfacing through the curated small-MT collections (no new MT prover failure);testMtStress= the quicksort load gap (new §18).jmltkbumped1.1.0-SNAPSHOT→1.2.1-SNAPSHOT(PR-author request). 1.2.1 parses the comment-form merge point (//@ merge_point …) into a new typedJmlMergePointStmt(ast.jml.stmt, new in 1.2.1) instead of leaving it an unparsed leftover comment; with no converter handler the default visitor aborts on the node'sjmlTagsSimpleName(A/B-verified: 1.1.0 green / 1.2.1 red,MergeRuleTests9× "Load failed"). Handled natively in53dcefd914:JP2KeYConverter.visit(JmlMergePointStmt)→MergePointStatementwith a temporary boolean location variable (like the fallback form), plus aJMLSpecFactory.createJMLMergeContractsoverload that re-serializes the node'smerge_proc/merge_paramsmetadata to the textualmerge_pointstatement and re-parses it with KeY's JML grammar — so parametric merge works natively, no leftover-comment fallback.MergeRuleTests12/12 +PredicateAbstractionLatticeTests3/3 under 1.2.1;speclang.*slice re-verified (299 tests, 2 failed = the two knownJMLParserExceptionTestcases, A/B-identical under 1.1.0/1.2.1, 10 skipped — no new failures).JMLTK_GAPS.mdre-measured at53dcefd914(4b62b1d6fa): key.core red count 14 → 11; §5 corrected (arrayMax/polishFlagSortare loop-invariant regressions, not\sumfidelity); §9 marked RESOLVED; §10 extended withTestReferenceSearcherand the node-40 root cause; §1 records the typed merge-point handling; new §17 documents the cosmetic[no file]origin term label (proof-irrelevant —OriginTermLabel.isProofRelevant() == false— causes no red job; documented, not fixed).testRunAllFunProofs/testRunAllInfProofsper-proof triage complete (9ad2c13bd1,854e6171f2). ThetestRunAll*jobs are CI-only, so the triage was done with local corpus runs at the branch tip (CI logs carry no failure messages).origin/main's Tests workflow is fully green — every Fun/Inf red is PR-induced by the front-end swap (they were invisible because the integration jobs were never part of the local baseline). The Fun set shrank 33 → 22 between the 1.1.0 (2026-11-02) and 1.2.1 (2026-11-08) CI runs — the 11 removed groups were fixed by the program/spec-shape commits. Classification (recorded inJMLTK_GAPS.md/TODO_CI.md):represents→ load failure (Funlist,javaCard,funOfIF,simple_info_flow,simpleTests; InfNewObjects) — JMLtk hits a hard ANTLR problem on the locset comma.quicksort) — JMLtk mis-reads//@ ghost \seq x = …as a class-level field.other,list_seq) — a proof saved under the JMLtk front-end carriesrequires @ [no file]origin strings thatOriginTermLabelFactory.parseOriginrejects (renderer/parser asymmetry), so reload-enabled groups fail; fix options recorded.ensures_redundantly→ load failure (FunSmansEtAl) — JMLtk accepts the standard-JML clause but KeY'sJmlParser.g4has no production, soJmlToTextualthrows "Unsupported clause kind".assignable_free→ load failure (Funjavadl) — the converter runs the symbol resolver on the clause keyword →UnsolvedSymbolException.perm.proofreplay drift (Funreload_examples) — the tracked proof loads but its recorded replay now has 6 errors (stored rule position no longer fits,One Step Simplificationnot reconstructable) — a stale recording against the new front-end, same family asrelax.proof.newBook,comprehensions,blockContracts,list_ghost,observer,example-algos,VACID0,VSTTE10,FM2024Tutorial,WeideEtAl,redux; InfToyVoting{,_fullmacro},ConditionalConfidential,SumExample*,ToyBanking{,_fullmacro},SimpleEvoting{,_fullmacro}) — need per-proof debugging; not a single root cause.SimpleEvoting_fullmacrois red in CI only (green locally — flaky, watching).Known degradation (accepted)
merge_pointis now covered for both forms (sincejmltk1.2.1,53dcefd914): the Java statementmerge_point(<expr>);(KeyMergePointStmt) is re-parsed as KeY'smerge_point_statement, and the comment form (//@ merge_point,merge_proc,merge_params) is parsed by JMLtk into a typedJmlMergePointStmtand converted natively — including parametric merge (merge_proc "MergeByPredicateAbstraction",merge_params {...}as used bytestcase/merge/*). TheKEY_JML_FALLBACKleftover-comment re-parse is no longer needed for merge points (it remains for the other KeY-specific constructs, e.g. proof scripts,nowarn/debugpragmas).JMLTK_GAPS.md(measured at53dcefd914, supersedesHANDOFF.md§5.2). Of the historical 34 recorded failures, the merge family,JmlScriptTest,Issue3452Test(KeY-side\seqname resolution, not a JMLtk gap) andTestProofStarterare green at HEAD (re-verified 2161/0); the record-goldens regression is fixed by the regeneration. Re-measured at53dcefd914(jmltk 1.2.1), the remaining recorded OPEN gaps are 9 failures: comma-separated store-refrepresents(4ScDeterminismTestload failures),\sum-proof fidelity (sum1.key/sum0.key), scripted-proof replay ofrelax.proof(3 tests:TestCopyingReplayer,TestEqualsModProofIrrelevancy, keyext.cachingTestReferenceSearcher), and the pre-existing block-contract combination bug (ParallelProverDeterminismTest); labeledbreak/continue(LoopScopeInvRuleTests) andarrayMax/polishFlagSortare resolved by6a07c20e63. In addition, the two knownJMLParserExceptionTestcases (not part of the recorded baseline) remain; further open entries inJMLTK_GAPS.md§12–§21 (absent grammar tokens,\strictly_nothing,[no file]origin labels, quicksort ghost locals,ensures_redundantly,assignable_free,perm.proofreplay drift) are not part of the recorded full-suite baseline. ThetestRunAll*corpus reds (22 Fun / 10–11 Inf groups, all PR-induced — see the 2026-11-08 bullet above) are likewise not part of the recorded baseline; they are the corpus-wide surface of the same gap families and need per-proof triage before this PR can claim corpus parity.Remediation: no silent spec weakening
Follow-up work on the shipped front-end (
242e6eb44d) that closes every path where a JML construct JMLtk accepts could be silently dropped, weakened, or mis-translated on its way through KeY's own JML grammar and term translation.JmlToTextualhard-fails on untranslatable clauses (KNOWN_GAPSstarts empty; skipping requires triaging the loss as acceptable), and the newJmlSideEffectCheckerstructurally rejects assignment operators,++/--, and object/array creation in JML specification expressions (set/ghost statements exempt; never descends into Java bodies). Wired into all contract/loop/class-level clause translations and theassert/assumebranch ofJP2KeYConverter.1.0.0lacks theast.jml.proofpackage (proof scriptsassert e \by { ... }), so the1.1.0-SNAPSHOT+ snapshots repository stay;build.gradlecomment tracks jmlparser-core 1.0.0 lacks ast.jml.proof (assert \by {...}) support shipped in 1.1.0-SNAPSHOT jmltoolkit/jmltk#82 for the pin-on-release path.StatementBlock/LoopStatement/MergePointStatementand a new atomicsetMergeContracts; the former racyremoveMergeContracts()+addMergeContract()sequences inProgVarReplaceVisitorandIntroAtPreDefsOpare gone (concurrent rule application never observes an empty contract set).JP2KeYConverterre-parses the JMLtkJmlProofStmtlist against KeY'sassertionProofgrammar intoKeyAst.JMLProofScript(assert and assume); a script JMLtk accepted but KeY cannot re-parse fails loudly instead of being dropped. Locked byAssertionProofScriptTest.SumClause/BsumClausefixtures assert\sumand\bsum(canonical(\bsum T v; from; to; summand)range form) survive the JMLtk → KeY re-parse verbatim;\bsumkeeps its loud deprecation warning.spec_*_mathpragmas restored. Class-level/*@ spec_java_math @*///*@ spec_bigint_math @*/in thespecMathfixtures are parsed by JMLtk as real modifiers and flow throughModifierKind.JML_SPEC_*intoJMLInfoExtractor;specMathJavaMathTest/specMathBigintMathTestare re-enabled andSpecMathModeTestlocks class, method and inline model-method modes.JMLTransformerrejects the datagroup family loudly (datagroup,in_group,maps_into,monitors_for,readable_if,writable_if,mapped_by,repr) instead of installing spurious fields, keepscaptures/duration/working_spaceas accepted drops, signals clauses omit the synthesized\exceptionbinder, and the information-flow serializer was rewritten to JMLtk's shifted getters withloop_determines/loop_separateswired to KeY's loop grammar. New negative/positive fixtures:WrongEquals(now a loudJmlSideEffectException),IncrementInContract,ObjectCreationInContract,NoSideEffects,Datagroup,DeprecatedDrops,NameClause(positive,[behavior] <name>:form),NameClauseClass(class-level legacyname "..."guard).Test status
8fe1be5b6c): twoJMLParserExceptionTestcases (MethodInMethod,ModelFieldinMethod— amodeldeclaration in a method body) fail; pre-existing and identical under the previous and the refreshed snapshot (KeY-side leftover-JML fallback gap, see the 2026-11-02 section).de.uka.ilkd.key.speclang.*slice: 299 tests, 2 failed, 10 skipped (measured at53dcefd914underjmltk1.2.1-SNAPSHOT; the 2 failures are the knownJMLParserExceptionTestpair, no new failures; before the 2026-11-02 fixture additions: 292/0/10 after the remediation commit242e6eb44d, the two previously-@DisabledspecMath*tests green again).KeyJavaPipelineTest(record code-transformation pipeline): 142 tests, 0 failures after the deliberate golden regeneration (102 → 108 expected files, incl. the new17_AnnotationMoverstage; 86 previously-differing goldens).MergeRuleTests12,MtMergePointTest1,TestTacletEquality2137,JmlScriptTest7,Issue3452Test2,TestProofStarter2 — 2161 tests, 0 failures.compileJava+compileTestJava(incl.key.uiand the keyext modules),spotlessCheckand the Checker-Framework nullness build (-DENABLE_NULLNESS=true compileTestJava): green.Note on the diff
The branch was rebased onto
origin/main, which already contains the JMLtk Java-parser migration (#3966, merged as8bd51f0e59). The PR diff therefore contains only the JML front-end work: the typed-JML-AST-based spec extraction plus thejmltkpin bump1.0.0→1.2.1-SNAPSHOT, the silent-spec-weakening remediation242e6eb44d(loud guards, proof-script/quantifier/spec-math parity, parallel-prover contract safety), and the recent pushed commitsf830558081(JMLTK_GAPS),a7a39edaa5(spec-case names),841b999eee(record-golden regeneration),a8f86ee351(measured-state docs update),8fe1be5b6c(nowarn/debug + datagroup-family fixtures),6a07c20e63(structural loop-invariant lookup),233ec1d9b0(pre-takeover program/spec shape for model methods and JML fields),53dcefd914(JMLtk 1.2.1 typed merge points + jmltk bump),4b62b1d6fa(CI triage recordTODO_CI.md+ JMLTK_GAPS re-measurement).Type of pull request
Ensuring quality
speclangtest-suite inkey.coreis the parity contract for the implementation and is green on the rebased branch (299/2/10 at53dcefd914underjmltk1.2.1-SNAPSHOT, the 2 failures being the knownJMLParserExceptionTestpair, no new failures);KeyJavaPipelineTestis green (142/0) after the deliberate golden regeneration; the previously-redkeyext.slicingmodule is green (17/17) andkeyext.cachinghas a single accounted failure (the recordedrelax.proofgap); whole-buildcompileJava/compileTestJava,spotlessCheckand the Checker nullness build are green at the branch tip; the remaining recorded gaps are tracked live inJMLTK_GAPS.md(supersedesHANDOFF.md§5.2) with zero new regressions.