Repository navigation
Conversation
Design (predicate.md) and executable checklist (predicate-impl.md) for the class-body `lemma` declaration (//@ instance lemma Pred(int i) = i > 0;): AST node, grammar, concrete syntax, validation, symbol resolution, tool backends and release steps.
…validation - New node JmlLemmaDeclaration in ast/jml/body (modifiers, name, parameters, body, jmlTags) extending JmlClassLevelDeclaration, registered in the metamodel generator; all generated visitors, metamodel and JavaToken kinds regenerated (LEMMA token added). - Grammar: <LEMMA: "lemma"> lexer token (JML states only), JmlClassLemma production and LOOKAHEAD(1) dispatch in JmlClassLevelInner; TokenTypes classification added. - Concrete syntax model entry and DefaultPrettyPrinterVisitor visit so genericPrettyPrint and toString round-trip the declaration. - ModifierValidator: allowed modifier set for lemmas (access, static, final, model, instance, pure, math modes), parameter modifiers and duplicate parameter-name detection. - Symbol-solver DefaultVisitorAdapter gains the throwing visit stub so the whole project still compiles.
- LemmaDeclarationTest: parse the motivating example (//@ instance lemma Pred(int i) = i > 0;), assert members/modifiers/params/body, toString and lexical-preserving round-trips, CSM round-trip without modifiers, and validator failures (duplicate parameters, disallowed modifier). - Fragment corpus: decl_jml_lemma_pred.txt (raw class-level JML). - Full example: fullexamples/tested/Predicates.java (processJml=true).
- JmlLemmaDeclarationContext resolves names in the lemma body against the formal parameters (JavaParserSymbolDeclaration.parameter), falling back to the surrounding class scope; registered in JavaParserFactory. - NameResolutionTest gains jmlLemma() against JmlLemmaResolutionTest.java, asserting body references (parameters lo/hi/i and a field) resolve with correct types.
- wd: WDVisitorExpr.visit(JmlLemmaDeclaration) delegates well-definedness to the lemma body expression. - stat: totalLemmas statistic key, reporter increment, and a <lemma> XML element with name/modifiers/body expression in the statistics visitor. - lsp: JmlCatchSymbols emits a Method DocumentSymbol for each lemma; CodeActionCollector offers the "Well-definedness Check" code action on the lemma body. - Tests: statistics counting, wd delegation (SExpr compared via toString), LSP document-symbol hierarchy and code-action presence.
- gradle.properties: 1.1.0-SNAPSHOT → 1.2.0-SNAPSHOT (feature ⇒ minor bump, fork-local SemVer per AGENTS.md). - jmltk-changelog.md: document the fork-local 1.x scheme with its mapping to the composite <JavaParser>-J<K>-K<KeY> releases, and add an unreleased 1.2.0-SNAPSHOT section listing the lemma-declaration feature.
Mark all completed phase checkboxes, keep push/PR open. Document deviations from the draft (NodeWithSimpleName, CSM modifiers() helper + no-modifier round-trip, validation tests in Phase 5, LEMMA token placement, generator ordering incl. the spotlessApply race, resolution context behavior, and the out-of-scope items).
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 |
Rename the JML class-body lemma declaration feature to 'predicate': keyword 'lemma' -> 'predicate', JmlLemmaDeclaration -> JmlPredicateDeclaration, token LEMMA -> PREDICATE, grammar production JmlClassLemma -> JmlClassPredicate, stat totalLemmas -> totalPredicates with <predicate> XML, and all tests/resources/doc prose renamed accordingly. - Regenerate grammar (compileJavacc), metamodel, visitors and concrete syntax (metamodel + core generators), spotless - Qualify ObservableProperty.PREDICATE in ConcreteSyntaxModel to disambiguate the new token constant - Update resolution test column markers (keyword grew 5 -> 9 chars) - KeY lexer (KeyDocumentHighlighter) and openjml/key corpus lemma uses are out of scope and untouched
wadoon
changed the title
//@ instance lemma Pred(int i) = i > 0;)//@ instance predicate Pred(int i) = i > 0;)
The predicate child node carries no stored line-ending style, so the default printer uses System.lineSeparator() (CRLF on Windows). Assert against System.lineSeparator() instead of a hardcoded '\n'. Pre-existing failure also present on the lemma version of the test.
This branch has not been deployed
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.
Summary
Adds JML class-body predicate declarations to the parser:
//@ instance predicate Pred(int i) = i > 0;.A predicate declares a named assertion formula over formal parameters that can be referenced from JML annotations. This PR implements the declaration itself (AST, grammar, printing, validation, resolution, tool backends). Proof scripts (
use_lemma), script bodies and body type-checking are explicitly out of scope.Implementation phases
Phase 0 — design (
2669b52ca)doc/design/predicate.md(design + language surface) anddoc/design/predicate-impl.md(executable checklist, completed).Phases 1–4 — core (
3fdd6dbae)JmlPredicateDeclarationinast/jml/body/extendingJmlClassLevelDeclaration, implementingNodeWithSimpleName,NodeWithModifiers,NodeWithAccessModifiers; fields/ctor order(jmlTags, modifiers, name, parameters, body).<PREDICATE: "predicate">lexer token (JML states only),JmlClassPredicateproduction (<PREDICATE> SimpleName() Parameters() "=" Expression() ";") dispatched viaLOOKAHEAD(1)fromJmlClassLevelInner;case PREDICATE:added toTokenTypes#getCategory.JavaTokenkinds + metamodel + all generated visitors regenerated.modifiers()list helper) andDefaultPrettyPrinterVisitorvisit sotoString()round-trips//@ instance predicate Pred(int i) = i > 0;.ModifierValidator: allowed modifier set (access,static,final,model,instance,pure, math modes), parameter modifiers, duplicate parameter-name detection.DefaultVisitorAdapterthrowing stub so the whole project compiles.Phase 5 — M1 tests (
916272a56)PredicateDeclarationTest(7 tests): parse + member assertions,toString()round-trip, lexical-preserving round-trip, CSM round-trip (modifier-less form), body/parameter AST, validator failures.decl_jml_predicate_pred.txt+ full examplefullexamples/tested/Predicates.java(both green inFragmentTest1335 cases /FullExamplesTest).Phase 6 — symbol resolution (
4decfae3b)JmlPredicateDeclarationContextresolves names in the predicate body against the formal parameters (JavaParserSymbolDeclaration.parameter), falling back to the enclosing class scope; registered inJavaParserFactory.NameResolutionTest.jmlPredicateagainstJmlPredicateResolutionTest.java(//?markers) verifies parameter + field resolution and types.Phase 7 — M3 tool backends (
830a5fb3d)totalPredicatesstatistic +<predicate name="…">XML element (modifier attrs + body expression stats).wd(body).DocumentSymbol(kindMethod) per predicate;CodeActionCollectoroffers the well-definedness check on the predicate body.Phase 8 — release (
a6cd3a564)gradle.properties→1.2.0-SNAPSHOT(feature ⇒ minor bump; fork-local SemVer perAGENTS.md);jmltk-changelog.mddocuments the fork-local 1.x scheme mapping and an unreleased 1.2.0 section.Phase 9 — QA (
c7a192b3e):jmlparser-core:test :jmlparser-jml-tests:test :jmlparser-symbol-solver-testing:test :jmlparser-core-testing:test :jmlparser-core-serialization:test :tools:wd:test :tools:stat:test :tools:lsp:test) green;spotlessCheck+checkstyleMaingreen (pre-existing warnings only); generator drift check: regenerate (compileJavacc→ metamodel generator → core generators) +spotlessApply→git diff --exit-codeclean.Phase 10 — rename
lemma→predicate(95581998c)lemma→predicate,JmlLemmaDeclaration→JmlPredicateDeclaration, tokenLEMMA→PREDICATE, grammar productionJmlClassLemma→JmlClassPredicate, stattotalLemmas→totalPredicates+<predicate>XML, and all tests/resources/doc prose.ConcreteSyntaxModelset-comprehension entry qualified asObservableProperty.PREDICATEto disambiguate the new token constant.//?column markers updated (keyword grew 5 → 9 chars).spotlessCheck+checkstyleMaingreen; drift check clean after regeneration.KeyDocumentHighlighter) andopenjml/keycorpuslemmauses are out of scope and untouched.Notes
jml_instancevia CSM (pre-existingPrintingHelperenum quirk, same as the reference branch); exact CSM round-trip uses the modifier-less form,toString()covers modifiers.spotlessApplyas separate gradle invocations (single invocation can race and produce false-positive drift).