Repository navigation
feat(core): KeY label-after-keyword JML statements (assert LAB: e;) + gap status doc - #86
Merged
Merged
Conversation
Contributor
Code coverage overviewLanguages: Java Java / code-coverage/jacoco-ubuntu-latest-21
View coverage of the 10 most impacted files.
ℹ️ Calculations represent line coverage. Results may change as calculations are updated. Updated |
…B: e;) Close syntax gap #5: extend JmlExpressionStmt with an optional label (SimpleName, @OptionalProperty) so formatted statements in KeY's form 'assert LAB: e;' / 'set SN: x = ...;' parse and round-trip, alongside the JML-standard prefix form (JmlLabelStmt). - grammar (java.jj JmlStatement): optional '[ LOOKAHEAD(<IDENTIFIER> ":") label=SimpleName() ":" ]' - printers: DefaultPrettyPrinterVisitor + ConcreteSyntaxModel emit the label - generated metamodel, visitors, and accessors regenerated (metamodel and code generators run in separate Gradle invocations) - regression tests: jmlparser-jml-tests JmlLabeledAssertTest
Document the empirically verified gap status (constructs 3, 4, 7 already parse; 5 fixed in the preceding commit; 1/6/8 skipped; 2 tracked on weigl/proofscripts).
wadoon
force-pushed
the
weigl/closinggaps
branch
from
October 29, 2026 23:45
e7f4ef5 to
8f948a9
Compare
wadoon
added a commit
that referenced
this pull request
Nov 1, 2026
…eam #86) Rebase onto origin/main brought in the KeY label-after-keyword feature (JmlExpressionStmt#label). Regenerate ModifierVisitor and VoidVisitorAdapter so the label is visited; output is byte-identical to what upstream main's codegen produces (verified against 42eded6). All other generated files were already consistent: the 682-file churn from the generators was pure license-header rewrites (generators emit COPYRIGHT_NOTICE_JP_CORE) and is reverted entirely by spotlessApply's licenseHeaderFile rule (gradle/header).
wadoon
added a commit
that referenced
this pull request
Nov 1, 2026
…nters DefaultPrettyPrinterVisitor and ConcreteSyntaxModel are hand-maintained (not emitted by :jmlparser-core-generators:run), so the rebase conflict resolution kept bf6adc6's pre-#86 versions and lost the KeY label-after-keyword support from origin/main (#86). Merge upstream's label emission back in: DPPV prints 'LABEL:' after the keyword, CSM adds conditional(LABEL, IS_PRESENT, ...). Restores JmlLabeledAssertTest#roundTripPrinting (assert LAB: x > 0; round-trips).
wadoon
added a commit
that referenced
this pull request
Nov 2, 2026
…eam #86) Rebase onto origin/main brought in the KeY label-after-keyword feature (JmlExpressionStmt#label). Regenerate ModifierVisitor and VoidVisitorAdapter so the label is visited; output is byte-identical to what upstream main's codegen produces (verified against 42eded6). All other generated files were already consistent: the 682-file churn from the generators was pure license-header rewrites (generators emit COPYRIGHT_NOTICE_JP_CORE) and is reverted entirely by spotlessApply's licenseHeaderFile rule (gradle/header).
wadoon
added a commit
that referenced
this pull request
Nov 2, 2026
…nters DefaultPrettyPrinterVisitor and ConcreteSyntaxModel are hand-maintained (not emitted by :jmlparser-core-generators:run), so the rebase conflict resolution kept bf6adc6's pre-#86 versions and lost the KeY label-after-keyword support from origin/main (#86). Merge upstream's label emission back in: DPPV prints 'LABEL:' after the keyword, CSM adds conditional(LABEL, IS_PRESENT, ...). Restores JmlLabeledAssertTest#roundTripPrinting (assert LAB: x > 0; round-trips).
wadoon
added a commit
that referenced
this pull request
Nov 2, 2026
After rebasing weigl/lsp onto main, the generated visitors/metamodel/printers carried the branch's pre-merge keyword-node versions and lost the element-quantifier (JmlQuantifiedVariable, #83) and KeY label-after-keyword (#86) visitor/CSM/printer additions that origin/main introduced. Restore the generator-consistent output (equal to the verified pre-rebase tip): GenericVisitor, VoidVisitor, the concrete visitor adapters, DefaultVisitorAdapter, and ConcreteSyntaxModel / DefaultPrettyPrinterVisitor keyword+label printing. Verified: :jmlparser-core:compileJava, scripts/run-generators.sh (git diff --exit-code clean), spotlessApply.
wadoon
added a commit
that referenced
this pull request
Nov 2, 2026
…eam #86) Rebase onto origin/main brought in the KeY label-after-keyword feature (JmlExpressionStmt#label). Regenerate ModifierVisitor and VoidVisitorAdapter so the label is visited; output is byte-identical to what upstream main's codegen produces (verified against 42eded6). All other generated files were already consistent: the 682-file churn from the generators was pure license-header rewrites (generators emit COPYRIGHT_NOTICE_JP_CORE) and is reverted entirely by spotlessApply's licenseHeaderFile rule (gradle/header).
wadoon
added a commit
that referenced
this pull request
Nov 2, 2026
…nters DefaultPrettyPrinterVisitor and ConcreteSyntaxModel are hand-maintained (not emitted by :jmlparser-core-generators:run), so the rebase conflict resolution kept bf6adc6's pre-#86 versions and lost the KeY label-after-keyword support from origin/main (#86). Merge upstream's label emission back in: DPPV prints 'LABEL:' after the keyword, CSM adds conditional(LABEL, IS_PRESENT, ...). Restores JmlLabeledAssertTest#roundTripPrinting (assert LAB: x > 0; round-trips).
wadoon
added a commit
that referenced
this pull request
Nov 2, 2026
After rebasing weigl/lsp onto main, the generated visitors/metamodel/printers carried the branch's pre-merge keyword-node versions and lost the element-quantifier (JmlQuantifiedVariable, #83) and KeY label-after-keyword (#86) visitor/CSM/printer additions that origin/main introduced. Restore the generator-consistent output (equal to the verified pre-rebase tip): GenericVisitor, VoidVisitor, the concrete visitor adapters, DefaultVisitorAdapter, and ConcreteSyntaxModel / DefaultPrettyPrinterVisitor keyword+label printing. Verified: :jmlparser-core:compileJava, scripts/run-generators.sh (git diff --exit-code clean), spotlessApply.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes the last open parser-level syntax gap to KeY from the closing-gaps pass (see
JMLTK_GAPS.md).What
assert LAB: e;/set SN: x = …;:JmlExpressionStmtgains an optionalSimpleName label(@OptionalProperty) + parser constructorjava.jjJmlStatement): optional[ LOOKAHEAD(<IDENTIFIER> ":") label=SimpleName() ":" ]DefaultPrettyPrinterVisitorandConcreteSyntaxModel(lexical preservation)jmlparser-jml-testsJmlLabeledAssertTest(6 tests)JMLTK_GAPS.md: empirically verified status of the remaining KeY syntax gaps:nullable(repair RangeExpressionTest #3),spec_*_math(Implement ghost labels #4),\strictly_nothing(Symbol resolution for JML constructs #7)merge_pointcomment form (fix RangeExpressionTest #1),nowarn/debug(Lambda Expressions #6), clause sugar (MethodDeclaration range #8)\byproof scripts (Bump actions/checkout from 6.0.2 to 7.0.0 in the deps group #2) →weigl/proofscriptsVerification
:jmlparser-jml-tests:test(full suite incl. new tests),:jmlparser-core:test,:jmlparser-core-testing:test,spotlessCheck,checkstyleMain— all green.