[wadoon]

Summary

Improvements to the JML parser/AST in javaparser-core and to the jmltk LSP server (tools/lsp), with follow-up updates across the lint, stat, redux, jmlstub, and utils tools.

JavaParser / JML AST (javaparser-core)

• Keywords are now first-class AST nodes. A new abstract base JmlKeywordNode (implements Jmlish) carries keyword values modelled by the JmlKeyword interface (jmlSymbol() / asString()):
  • JmlContractBehavior holds the behavior keyword introducing a contract (behavior, normal_behavior, exceptional_behavior, model_behavior, break/continue/return/abrupt_behavior, …), resolving from the parsed token incl. British spellings (*_behaviour) and feasible_behavior → behavior.
  • Clause and body-clause keywords are now child nodes of their clause: JmlClauseKind (wrapping JmlClauseKeyword, e.g. requires/ensures/assignable/signals/forall) and JmlBodyClauseKind (wrapping JmlBodyClauseKeyword, e.g. invariant/constraint/axiom/initially). This gives every keyword a token range, which the LSP uses for document symbols and code actions.
• API changes that follow from this (breaking for downstream users, in particular KeY):
  • com.github.javaparser.ast.stmt.Behavior is removed; JmlContract now stores a JmlContractBehavior node or null instead of Behavior.NONE for contracts without a behavior keyword. JmlContract.getBehavior() returns Optional<JmlContractBehavior>, behavior() is now @Nullable.
  • JmlClause subclasses no longer keep their own kind field; the keyword node is a regular child (getKind() returns the JmlClauseKind/JmlBodyClauseKind node), so child-node counts of clauses change by one.
  • abrupt_behavior now maps to its own JmlBehaviorKeyword.ABRUPT instead of being folded into BREAK.
  • Node.associatedSpecificationComments and ObservableProperty.ASSOCIATED_SPECIFICATION_COMMENTS are removed (the parser never populated them).
  • Node.treeIterator is now public.
• Grammar (java.jj): clause productions for forall, signals, signals_only and the behavior productions now build the keyword nodes; loop/model contracts pass null behavior where none is present.
• Error positions for malformed local variable declarations: the BlockStatement lookahead for variable declarations was rewritten to Modifiers() Type() Identifier() (ArrayBracketPair())* ("," | "=" | ";"), so a syntactic lookahead no longer swallows the parse error. Malformed declarations such as int i = ; are now reported at the offending token instead of the statement start (regression test VariableDeclarationErrorPositionTest, jmltk#71).
• Regenerated metamodel, JavaParserMetaModel, visitors, and pretty-printers (DefaultPrettyPrinterVisitor, PrettyPrintVisitor, ConcreteSyntaxModel — the keyword nodes print their value symbol).
• Javadoc added to the JML container/contract interfaces (JmlContainer, NodeWithContracts, HasJmlTags, …); metamodel generator registers the new node types and drops dead commented-out entries.
• Small symbol-solver adjustment (DefaultVisitorAdapter handles the new keyword nodes) and lexical-preservation test fix (Issue2620Test).

LSP server (tools/lsp)

• Actions reworked to a common LspAction interface discovered via ServiceLoader (registered in META-INF/services), supporting both client-applied snippet edits (SnippetTextEdit) and server commands.
• New code actions:
  • AddBehaviorKeyword — inserts a missing behavior keyword before a contract (snippet with choices).
  • AddNameToClauseOrContract — inserts name: labels for unnamed contracts, clauses and class-level declarations.
  • AddQuantification — wraps a JML expression around the cursor into (\forall <type> <name>; …).
  • AddStubs — code lens on types (stub generation, still to be implemented).
• Reworked actions: WellDefinednessCheck, VerifyAgainstParent, CreateKeyProjectFile (now writes project.key into the workspace root); StartKey removed.
• Document symbols: extended JmlCatchSymbols (contracts, clauses, JML fields/represents/accessible declarations) and KeyCatchSymbols (function declarations, predicates, schema variables, taclets).
• Server/launcher: custom Launcher construction with executor service, message validation, new --trace [-|file] option, tcpNoDelay + keepAlive on sockets (stdio/server/client modes).
• Semantic-token registration now covers **/*.{jml,java} and **/*.key.
• Docs: expanded doc.md (JML clause reference), new sol.md (KeY sol-terms reference); added eglot.el for editor testing.

Other tools

• lint: rules adapted to the keyword nodes (AllowedJmlClauses, AssignableValidator, ResultVarCheck); ContextSensitiveForbiddenFunctionsValidator moved to the io.github.jmltoolkit.lint.rules package (service registration updated).
• stat: StatVisitor / Statistics / StatisticKeys use the renamed keyword nodes.
• redux: RecordClassBuilder builds JmlBodyClauseKind nodes for the generated equals/hashCode invariants.
• jmlstub: JREClassStubGenerator emits JmlContractBehavior/JmlBehaviorKeyword.
• utils: new JMLUtils.isInJML, findTopMostAncestor[Consecutive], and Helper.findAll helpers.

Tests

• New: VariableDeclarationErrorPositionTest (grammar error positions), CodeActionsUnitTest (all new actions + collector defaults), JmlCatchSymbolsTest, KeyCatchSymbolsTest, CodeActionCollectorTest.
• Updated: JKIssue (clauses now carry the keyword node as child), JmlLambdaExprTests, JmlStatisticsReporterTest.

Known limitations

• WellDefinednessCheck and AddStubs are advertised but not yet implemented (executing them reports "not yet implemented"); the snippet insertion of AddBehaviorKeyword still needs polishing.

[github-code-quality]

Code coverage overview

Languages: Java

Java / code-coverage/jacoco-ubuntu-latest-21

main cbb924b	weigl/lsp 3da7c78	+/-
57%	58%	+1%

View coverage of the 10 most impacted files.

File	main cbb924b	weigl/lsp 3da7c78	+/-
com/github/java...ierVisitor.java	55%	58%	+3%
com/github/java...torAdapter.java	51%	59%	+8%
com/github/java...odeVisitor.java	51%	62%	+11%
com/github/java...odeVisitor.java	49%	60%	+11%
com/github/java...torAdapter.java	60%	72%	+12%
io/github/jmlto...CatchSymbols.kt	47%	66%	+19%
com/github/java...useKeyword.java	0%	92%	+92%
io/github/jmlto...seOrContract.kt	0%	94%	+94%
io/github/jmlto...aviorKeyword.kt	0%	96%	+96%
io/github/jmlto...CatchSymbols.kt	0%	100%	+100%

ℹ️ Calculations represent line coverage. Results may change as calculations are updated.

---

_{Updated October 17, 2026 16:04 UTC}

[wadoon]

Review of PR #61 (weigl/lsp)

Reviewed the full diff (~135 files). The generated visitor/metamodel/pretty-printer churn is consistent (the "Metamodel/Model are fresh" CI check is green), and I focused on the hand-written changes: the grammar change, the new keyword-node AST classes, and the LSP code actions. CI is fully green. Findings below; nothing here blocks the AST-side changes, but the LSP findings (1)–(3) are worth fixing before the code actions ship to users.

1. AddNameToClauseOrContract crashes the whole codeAction request for unsupported declarations (moderate)

tools/lsp/src/main/kotlin/io/github/jmltoolkit/lsp/actions/AddNameToClauseOrContract.kt

• isCallableForNode accepts every JmlClassLevelDeclaration subclass: JmlFieldDeclaration, JmlMethodDeclaration, JmlRepresentsDeclaration, JmlClassAccessibleDeclaration, JmlClassExprDeclaration.
• hasName() only handles JmlContract / JmlClause / JmlClassExprDeclaration; everything else falls into else -> false, so an action is offered even for nodes that already have a name.
• createEdit()'s when handles only JmlContract / JmlClause / JmlClassExprDeclaration and throws error("Unexpected node: $node") for the rest — i.e. an IllegalStateException for exactly the node classes that pass isCallableForNode.

CodeActionCollector.collect has no per-action error handling, so the exception propagates out of textDocument/codeAction and the client gets a failed request (no code actions at all for that document/range).

Realistic trigger: cursor on a position covered by such a declaration but not by any child range — e.g. on the trailing ; of //@ ghost int x;, or inside model void m(); in a token gap. Suggested fix: restrict isCallableForNode to JmlContract || JmlClause || JmlClassExprDeclaration, or actually handle the remaining types in hasName/createEdit.

2. AddBehaviorKeyword inserts a malformed snippet (moderate)

AddBehaviorKeyword.kt:67:

" \${1:${JmlBehaviorKeyword.entries.joinToString("|") { it.jmlSymbol() }}: "

produces ` ${1:|behavior|normal_behavior|…|return_behavior: ` — three problems:

• NONE("") is part of entries, so the choice list starts with an empty |behavior… entry;
• VS Code choice syntax is ${1|a,b,c|}, not ${1:a|b|c:;
• the placeholder is never closed (and there's a stray trailing : ).

So the quick fix inserts broken text. The unit test only asserts contains("normal_behavior"), so it doesn't catch this. Suggested: " \${1|${entries.filter { it != NONE }.joinToString(",") { it.jmlSymbol() }}|}" (note , separators for choices, and a closing |}).

3. Unhandled exceptions inside code-action computation fail the entire request (moderate)

CodeActionCollector.createCodeAction calls it.createCodeAction(uri, node) with no try/catch. Two concrete throwing paths:

• Finding 1 above (error(...)).
• AddQuantification.kt:51 calls node.calculateResolvedType() unguarded. With the LSP's CombinedTypeSolver this throws UnsolvedSymbolException for names the solver can't resolve — common in JML-only code (ghost/model variables of other classes, spec-only identifiers). The test only exercises a resolvable name (size → field of the same class).

Suggestion: wrap each action's createCodeAction/createCodeLens call in a try/catch that logs and skips, so one bad node/action degrades to "no action" instead of a failed request.

4. Advertised but unimplemented commands (low–moderate)

• WellDefinednessCheck.createCodeAction offers a QuickFix command on JmlSimpleExprClause / JmlSignalsClause / JmlClassExprDeclaration / JmlExpressionStmt; executing it reaches execute(server, uri, range) → TODO("Not yet implemented") → NotImplementedError surfaces as an LSP error for the user. The test only covers the value == null guard.
• AddStubs registers a code lens on every type declaration (and a command(uri, target) entry point), but execute ends in TODO("Provide the return value") (the when (node) branches are empty scaffolding).

If these aren't ready, consider not offering them yet (return null from createCodeAction/createCodeLens) so users don't get error dialogs.

5. VerifyAgainstParent cache is never populated (low)

The createCodeLens override (which did cache.put(node.hashCode(), node)) was removed and the CodeLensCollector call is commented out, so the Guava cache is now dead. Executing the offered command does cache.getIfPresent(...) → always null → silently returns "" (previously it at least showed "Prove is not implemented yet."). Either populate the cache in createCodeAction, or pass URI/range as arguments instead of a node hash.

6. Minor cleanups

• main.kt: the commented-out TeeInputStream/TeeOutputStream block can be deleted.
• CreateKeyProjectFile.command(rootUri: String): WorkspaceEdit is now unused (only the interface command() is used).
• RecordClassBuilder.kt: unused import com.github.javaparser.JavaToken.Kind.INVARIANT_FREE.
• AddStubs.kt: several unused imports (Gson, MethodDeclaration, CharsetDecoder, …); GsonHelper might deserve its own file.
• JmlKeywordNode<S extends Node>: the type parameter S is never used in the class; the javadoc also refers to "type parameter {@code T}".
• tools/lsp/eglot.el is a personal editor config with an absolute /home/weigl/… path — double-check it's meant to be committed.
• javaparser-key-generator/.../CopyNodeGenerator.java still has a case "associatedSpecificationComments": for a property removed in this PR (now dead).

7. Pre-existing issues carried into the renamed enum (optional drive-by)

The JmlClauseKeyword enum is a 1:1 move of the old JmlClauseKind, so these two are not introduced by this PR, but since the enum was rewritten here:

• DETERMINES, LOOP_DETERMINES, SEPARATES, LOOP_SEPARATES all reference GeneratedJavaParserConstants.DURATION_REDUNDANTLY; the matching token constants (DETERMINES, …) exist in the grammar. Harmless today (getTokenType() is unused; resolution goes by symbol), but wrong.
• DECREASING_REDUNDANTLY is accepted by JmlDecreasesClause in the grammar but has no enum entry, so getKindByToken throws IllegalArgumentException and //@ decreasing_redundantly 1; can't be parsed (identical behavior on main).

What I checked and found sound

• Grammar lookahead rewrite (BlockStatement): the new LOOKAHEAD(Modifiers() Type() Identifier() (ArrayBracketPair())* ("," | "=" | ";")) matches exactly the prefix shape of the first declarator, so statement classification for well-formed input is unchanged; malformed declarations now report the offending token instead of the statement start. The new VariableDeclarationErrorPositionTest pins this.
• JmlBehavior() → JmlContractBehavior mapping: all grammar tokens are covered by JmlBehaviorKeyword.getByToken, including British spellings, feasible_behavior → BEHAVIOR, and model_behavior; abrupt_behavior now maps to its own ABRUPT keyword instead of being folded into BREAK (old behavior — worth noting as a small semantic change).
• Contracts/loop contracts without a behavior keyword pass null into the @OptionalProperty behavior field — the regenerated JmlContract handles this (getBehavior() → Optional).
• All class-level body-clause tokens (axiom/invariant*/initially/constraint*) are covered by JmlBodyClauseKeyword.
• ServiceLoader registrations updated (7 LSP actions; lint rule package move to io.github.jmltoolkit.lint.rules).
• ConcreteSyntaxModel gained attribute(VALUE) entries for the three keyword-node classes; visitors/pretty-printers regenerated (freshness check green).
• WellDefinednessCheck/VerifyAgainstParent command ids unchanged, so existing client-side bindings still work.