Skip to content

Feature/jml syntax parser - #230

Open
JaferShar wants to merge 4 commits into
devfrom
feature/jml-syntax-parser
Open

JaferShar wants to merge 4 commits into
devfrom
feature/jml-syntax-parser

Conversation

@JaferShar

Copy link
Copy Markdown
Collaborator

Added a JML Syntax Parser that detects JML syntax errors and displays a meaningful text underneath the afflicted condition.
Syntax errors can be e.g. an assignment = instead of ==, unbalanced parentheses, missing operands (a >), unknown JML keywords (\result), quantifiers not in the supported form (\forall int i; (…)) or integer literals that are too large for a Java int.

Parser

  • Mirrors the grammar of the backend ConditionParser, so a condition that is valid in the frontend can also be parsed by the backend.
  • Additionally reports input the backend accepts but silently mangles:
    • trailing tokens are dropped (a > b c becomes a > b, A[i].length becomes A[i])
    • unary operators used as binary ones (a ! b)
    • a trailing comma in predicate calls (pred(a,))
grafik

The spec did not compile, as the condition input is a BehaviorSubject
and the colored condition tokens were not provided.
Port of the backend condition grammar, so that conditions accepted in
the frontend can also be parsed by the backend. Additionally reports
input the backend silently mangles: trailing tokens, unary operators
used as binary operators and a trailing comma in predicate calls.
Long input is shortened in the messages.
Invalid conditions get a red border and the error message in a card
below the field. Loaded conditions are checked immediately, changes
after a pause of 2 seconds or when leaving the field, in all editors
showing the condition. Program statements are not checked.

The message does not shift the statement and does not react to clicks.
Every statement reserves invisible space below it for the message, as
content outside of a node is not reliably repainted by the browser.
Bottom handles are moved up by this space to stay at the border of the
statement.
…/jml-syntax-parser

# Conflicts:
#	frontend/src/app/components/editor/condition/condition-editor/condition-editor.component.ts
@JaferShar JaferShar linked an issue Sep 30, 2026 that may be closed by this pull request

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Frontend parsing for JML syntax

1 participant