Repository navigation
feat: element-domain quantifiers over arrays, ranges and Iterables - #83
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 |
wadoon
force-pushed
the
weigl/quantarray
branch
2 times, most recently
from
October 30, 2026 13:17
61f0a6a to
4e3f2c5
Compare
…Binding parent + foreach binding node)
…inimal-ripple alternative analysis)
…pe to single iterable bindings
…ntified bindings) New AST node com.github.javaparser.ast.jml.expr.JmlQuantifiedVariable extends VariableDeclarator with an optional iterable domain property. Registered in MetaModelGenerator.ALL_NODE_CLASSES; metamodels, visitors, and node methods regenerated (JmlQuantifiedVariableMetaModel extends VariableDeclaratorMetaModel). Generator fix: NodeMetaModelGenerator only emitted the protected 6-arg metamodel constructor for abstract nodes; VariableDeclarator is the first concrete node to gain a subclass, so MetaModelGenerator now passes hasSubclasses into the per-node generation. Printers unblocked post-regeneration (CONTRIBUTING step 3-4): DefaultPrettyPrinterVisitor.visit(JmlQuantifiedVariable) prints 'type name : iterable', and visit(JmlQuantifiedExpr) skips the common-type scheme for bound bindings; PrettyPrintVisitor and the symbol-solver DefaultVisitorAdapter got stubs. customInitialization() overridden to avoid double observer registration. Design: doc/design/quantarray.md (v4) + doc/design/quantarray-impl.md (Phase 1).
…pe print for bound lists
ConcreteSyntaxModelTest requires an entry for every metamodel node, so the
Phase 3 CSM work is pulled forward:
- ConcreteSyntaxModel: add JmlQuantifiedVariable entry ("type name : iterable")
and restructure the JmlQuantifiedExpr entry so the leading common type is
printed conditionally on getMaximumCommonType() being present - bound
bindings (JmlQuantifiedVariable) print their own type, avoiding a double
space for the classic scheme.
- JmlQuantifiedExpr.getMaximumCommonType(): override (marked @DerivedProperty so
the metamodel registration survives regeneration) that reports the derived
common type as absent when any binding carries an iterable domain.
Drift check passes: metamodel-gen + core-gen + spotlessApply reproduce the
committed state byte-for-byte.
java.jj, JmlPrimaryPrefix() quantifier alternative: after QuantifiedVariables() accept an optional ':' iterable=Expression(). A declared iterable binds exactly one variable (multi-declarator lists raise a ParseException with a fix-it message), and the declarator is re-wrapped as JmlQuantifiedVariable(type, name, iterable). 'var' types (no type args, no array levels) normalize to VarType, so (\forall var e : a; e != null) parses. VarValidator: 'var' in a JmlQuantifiedVariable is legal (type inferred from the iterable element type by later symbol-solver phases); exempted so parsing succeeds. No new tokens — TokenTypes untouched. compileJavacc: 0 errors; full :jmlparser-core-testing suite green.
…fiers JmlProcessor.JmlReplaceVisitor (runs when processJml=true) gains: - visit(JmlQuantifiedVariable): a bound binding must not carry an initializer (grammar now preserves it via the 4-arg constructor instead of silently dropping '= 3'), and the iterable domain must not reference the bound variable (NameExpr scan — member-access component names such as 'list.e' are correctly NOT flagged; self-index sugar stays deferred). - visit(JmlQuantifiedExpr): defensive check that a quantifier with an iterable-bound binding carries exactly one variable (the grammar already rejects this at parse time). Verified in jshell (processJml=true): positive forms (classic, var, range 0..n, member-access domains) parse clean; a[e], e = 3, e.length all report the expected problem. :jmlparser-core-testing:test and :jmlparser-jml-tests:test green.
- jml-exprs.txt: 10 positive forms (element, var-typed, generic T, sum, num_of, min, multi-expression, range 0..a.length-1, int[], nested exists) parsed by JmlExpressionTest. - csm_jml_expression.txt: same 10 for the CSM round-trip; range example spaced to canonical form (0 .. a.length - 1), the other nine round-trip verbatim. - QuantifiedExprValidationTest: negatives with processJml=true — multi-declarator + iterable (parse-level), self-referencing iterable a[e], initializer-bound e = 3 (JmlProcessor-level) — plus a positive control. - LexicalPreservingPrinterTest: contract with a bound and a range-domain quantifier round-trips byte-for-byte. - fullexamples/tested/QuantArray.java (FullExamplesTest, processJml=true) + fragments/decl_quantarray_iterable.txt (FragmentTest). All module tests green.
…dings JmlJavaParserQuantifiedVariableDeclaration.getType() now derives the bound variable's type from the iterable domain (the same rule VarType.convertToUsage applies to enhanced-for variables): - range 0..n -> int - array -> component type (element of T[][] is T[]) - generic reference type (Iterable/SequencedCollection, ...) -> first type argument; raw domain -> java.lang.Object - unresolvable domain -> declared type as fallback This makes (\forall var e : a; ...) and (\forall T e : c; ...) resolvable; JmlQuantifiedExprContext.solveSymbol is unchanged (classic loop still works, it already delegates to JavaParserSymbolDeclaration.quantifiedVar). Tests: NameResolutionTest.jmlBinderExpressionIterable (new //? expectation file covering array / int[][] / List<String> / var / range / shadowing) and QuantifiedVariableTypeInferenceTest asserting the inferred type VALUES. Full :jmlparser-symbol-solver-testing:test and :jmlparser-jml-tests:test suites green.
…ackends JmlQuantifierDesugarer rewrites single-binding element quantifiers to the classic index form: range domains (kind 2) become a half-open bound filter, array domains (kind 3) become a fresh-index loop over a.length with the bound variable substituted by a[_i] (binder and filters preserved). Kinds are decided syntactically for ranges and via calculateResolvedType for arrays; Iterable domains (kind 4) and unresolvable domains degrade to Optional.empty(). Used by the KeY path and the LSP quick-fix. jml2java: bound element bindings now translate to enhanced-for (array / Iterable) or an index loop (range), with \sum/\product/\num_of accumulation (result_N && pred_M for forall, sum_ += v, ++num_ guarded by the filter). The classic while-loop path is kept byte-identical; a temporary print test captured the exact outputs into expr.yaml fixtures.
Element quantifiers over arrays (kind 3) and ranges (kind 2) are now desugared via JmlQuantifierDesugarer and re-encoded through the classic forall path, yielding (forall ((_i Int)) (=> (and (<= 0 _i) (< _i (int$length ary))) ...)). Iterable domains (kind 4) fail loudly with an UnsupportedOperationException instead of silently mis-encoding. Also fixes SmtTermFactory.list(List<SExpr>), which was a stub dropping the forall/exists binder variables (the reason the classic quantifier expr.yaml fixture was disabled) — that fixture is re-enabled as a regression.
Element-domain quantifiers now require the iterable domain itself to be well-defined (non-null, free of NPEs/division by zero, evaluated once) in addition to the well-definedness of the bound filters and body. Adds wd and not-wd CSV fixtures covering a well-defined array domain, a range domain, remainder-in-body, a division-by-zero domain, and division-by-zero in the body.
Adds StatisticKey.totalElementQuantifiers plus a per-binder BINDER_ELEMENT_<sym> counter, incremented for single-binding quantifiers whose binding carries an iterable domain (kind 2-4). Classic quantifiers keep counting only into totalQuantifiers/BINDER_<sym>.
CodeActionCollector now offers an 'Expand quantifier domain' code action for element-domain quantifiers of kinds 2 (range) and 3 (array), rewriting them to the classic index form via JmlQuantifierDesugarer; kind 4 (Iterable) and unresolvable domains degrade to no action and never crash the collector.
SpotlessApply touched the new Phase 7 files (license headers where missing, line wrapping, blank lines between when branches); spotlessCheck and checkstyleMain are green for every touched module.
jmltk-changelog.md: document the fork-local SemVer scheme as current (1.0.0 = 3.28.2-J8.0-K13.6) with the composite scheme as history, add an Unreleased — 1.2.0-SNAPSHOT entry for the quantarray feature (Phases 1-7 with commit hashes), and extend the version-history table with the 1.0.0 / 1.1.0-SNAPSHOT states. gradle.properties: version=1.2.0-SNAPSHOT (feature ⇒ minor bump). Full corpus (FragmentTest, FullExamplesTest) green; root spotlessCheck + checkstyleMain green (pre-existing warnings only in unrelated modules); all touched module suites re-run green.
… (Metamodel/Model are fresh) The codegen reprint moves trailing same-line comments inside CSM sequence(...) calls left by one element on every regeneration (space() -> attribute(BINDER) -> token(LPAREN)), so no in-sequence placement is a fixpoint. Move the explanation of the conditional MAXIMUM_COMMON_TYPE print to standalone comment lines above the put(...) statement, which the generator round-trip preserves (verified: generators + spotlessApply reproduce the committed tree byte-for-byte).
wadoon
force-pushed
the
weigl/quantarray
branch
from
October 31, 2026 16:36
4e3f2c5 to
40912bf
Compare
wadoon
commented
Oct 31, 2026
Addresses review comments on #83: - JmlProcessor.JmlReplaceVisitor: remove the visit(JmlQuantifiedExpr) defensive check. The grammar (java.jj) already rejects an iterable domain with != 1 variables via ParseException, so the check was dead for parser-produced ASTs and did not belong in the JML processing pass. QuantifiedExprValidationTest#iterableBindsExactlyOneVariable keeps passing through the parse-level error. Design docs updated: quantarray.md 3.6 drops the 'defensive validator' note; quantarray-impl.md Phase 4 marks the multi-declarator case as grammar-enforced only. - VarValidator: the exemption comment claimed the type 'is inferred from the iterable domain's element type'. Clarify: (\forall var e : a; ...) is allowed and denotes the domain's element type (equivalent to (\forall T e : a; ...) with T the element type); the declared type stays 'var' in the AST and resolving it is the symbol solver's job.
Adds fullexamples/tested/GhostArrayQuantifier.java (FullExamplesTest, processJml=true) covering the pattern from the PR discussion: a //@ ghost int[] field with an initializer, an element-domain class invariant and ensures clause, and a method-body assert (\forall int e : array; e > 0). The binding parses as a JmlQuantifiedVariable with an array (kind 3) domain; full example runs green (0 problems).
Contributor
Author
|
Added as a full-example test case (commit It covers the discussed pattern — a |
wadoon
added a commit
that referenced
this pull request
Nov 1, 2026
wadoon
added a commit
that referenced
this pull request
Nov 2, 2026
…(P3.2) \forall/\exists/\sum with an element or range domain (e.g. '(\forall int e : a; e > 0)', stored on JmlQuantifiedVariable per the merged core #83) have no VCG desugaring: the old path bound the variable by its declared type and translated the body, silently *dropping the domain* — '(forall ((e Int)) (> e 0))' — an unsound encoding (the requires collapses to false assumptions). checkSupported now aborts such quantifiers with a structured UnsupportedFeatureException naming the binding form, matching the existing loud-rejection policy. VcgSemanticsTest: two new unsupportedConstructs rows (quantIterableDomain, sumIterableDomain); suite 333->335, all green (vcg 873, cli 4).
Open
wadoon
added a commit
that referenced
this pull request
Nov 2, 2026
…changelog policy Resolves the 16-file conflict between PR #61's regenerated visitor set and main's #83 (JmlQuantifiedVariable) visitors by regenerating from the merged sources: the 15 ast/visitor files are now the true union (branch keyword nodes + #83's quantified-variable visits). The hand-maintained printers (ConcreteSyntaxModel, DefaultPrettyPrinterVisitor) keep the auto-merged union; their earlier rewrites came from the generators' reprint, which spotlessApply normalizes away. CodeActionCollector keeps the branch's action-table object design: the auto-merged JmlTextDocumentService already commits to CodeActionCollector.collect(uri, node). #83's quantifier quick-fixes are ported onto it as AddBoundary and ExpandQuantifierDomain LspActions (isCallableForNode stays class-pure, per-node decisions live in createCodeAction), and main's ElementQuantifierCodeActionTest is rewritten to the object API (same assertions, exact titles). Suites all green: jml-tests 1806, lsp 54, lint 28, smt 35, stat 35, wd 17, jml2java 28; spotlessCheck + checkstyleMain pass. Changelog gains the PR #61 LSP entry under Unreleased 1.2.0-SNAPSHOT (version bumped by #87).
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
The rebase onto main dropped the AddBoundary and ExpandQuantifierDomain action classes (and their ServiceLoader registration) and reverted ElementQuantifierCodeActionTest to the pre-adaptation form that instantiated the class-based CodeActionCollector. Restore the action-table versions from the pre-rebase tip: collector as object, expand via JmlQuantifierDesugarer, adapted test using CodeActionCollector.collect.
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
The rebase onto main dropped the AddBoundary and ExpandQuantifierDomain action classes (and their ServiceLoader registration) and reverted ElementQuantifierCodeActionTest to the pre-adaptation form that instantiated the class-based CodeActionCollector. Restore the action-table versions from the pre-rebase tip: collector as object, expand via JmlQuantifierDesugarer, adapted test using CodeActionCollector.collect.
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.
Element-domain quantifiers over arrays, ranges and collections
Implements the quantarray design (
doc/design/quantarray.md,doc/design/quantarray-impl.md): JML quantifiedexpressions with a single-binding element domain over arrays, ranges (
\forall int i; 0 <= i && i < a.length; P—actually
\forall int i; i < a.length; Pafter desugaring is covered by the classic index form) andIterable/SequencedCollectiondomains.Syntax
int i, T e : a[i](index+element multi-binding) is explicitlydeferred (see design v4, commit
b83a3e2c4).\forall T e : a; P→\forall int _i; 0 <= _i && _i < a.length; P(a[_i])with a fresh, escalated_i), preserving the original binder.Iterable/SequencedCollectiondomains keep a dedicated element form and are handled in each backend withoutdesugaring.
What's included (Phases 1–8)
a00227144…d9fe01286JmlQuantifiedVariableAST node (extendsVariableDeclarator), iterable-domain quantified bindings8df3526a821e69bcafjava.jj)1bdf833d8153591665f2d67de0fjmlparser-jml-tests)249c8fd05ef6c8328958dbc6ad7tools/smt) +SmtTermFactorybinder fixc622f256a1ea5178e9totalElementQuantifiers, per-binderBINDER_ELEMENT_*)0c894f223da1a4fba72d1fd073c1.2.0-SNAPSHOT, corpus (FragmentTest,FullExamplesTest) green4b76b9cf5Backend behavior
JmlQuantifierDesugarer): range/array domains → classic index form with fresh_iindex(escalating
__i,___i, …); binder preserved;Iterablenever desugared.Jml2JavaTranslator): syntactic branch on element binder + iterable domain — range → index loop,array/
Iterable→ enhancedfor; element\forallemitsresult_N = result_N && pred_M; classicwhile-loop emission stays byte-identical to before.
JmlExpr2Smt): range/array desugared → re-dispatched on the classic form (parent wired viasetParentNodeso resolution works); element-form remains unsupported →UnsupportedOperationException.wd(iterable)∧wd(all bound expressions)(nosmtFormulaon bound variables).
Verification
javaparser-core,javaparser-core-testing,javaparser-symbol-solver-testing,jmlparser-jml-testsand all touched tool modules (
tools/jml2java,tools/smt,tools/wd,tools/stat,tools/lsp)test suites green.
spotlessCheckandcheckstyleMaingreen (only pre-existing warnings in generator modules)../scripts/run-generators.shregenerates code; generated files are not hand-edited.Diff: 19 commits · 60 files · +2662 / −19
Note: PR base is
main; this is a fork-local feature branch (weigl/quantarray) as per theCONTRIBUTING.mdworkflow.