JmlLexer w/o expr mode

[wadoon]

Intended Change

Make JMLLexer more straightforward to understand by eliminating the two modes (aka contract/expr or outer/inner).

Type of pull request

• Refactoring (behaviour should not change or only minimally change)

Ensuring quality

• I have tested the feature as follows: unit-tests

Breaking Changes

• Identifier that clashes with JML keywords need to be quoted now.

[wadoon]

I just re-noticed how bad the JML language design is.

  /*@ model_behavior
        accessible<heap> fpLock();
        accessible<permissions> fpPerm();
  ...

The previous JML contract could mean:

• A model contract with the two accessible clauses.
• An empty model contract, and the definition of the method fpLock returning an instance of accessible<heap>. Followed by a second method definition.

[mattulbrich]

An empty model contract, and the definition of the method fpLock returning an instance of accessible<heap>. Followed by a second method definition.

Would that not require the keyword model before the method declaration? There are no method declarations in comments without model (or possibly ghost one day).

[wadoon]

Would that not require the keyword model before the method declaration? There are no method declarations in comments without model (or possibly ghost one day).

model is a modifier, and therefore admissible currently. This should be valid lexically:

//@ model model model(model model model) { return model; }

A model method, named model, getting a model instance (named model), and returning it.
It should be rejected because model is not a valid identifier for parameters (currently not in KeY bit in the jmlparser), but ghost is valid on parameters (if your plans are accepted):

//@ model model model(ghost ghost ghost) { return ghost; }

[wadoon]

Discussed solutions:

1. Introduce two parser rules for identifier: one for relaxed identifier (Java identifier + JML keywords) and one for strict identifiers (Java identifier only).

   Use strict identifiers in ambiguous positions. Nobody needs to declare a model method which collides with a JML name.

   This does not work as names in Java can collide with JML names. You can then never declare a model method return the class invariant.

2. Introduction of backticks to quote JML keywords.

3. Remove ghost and model from the list of modifiers.

   Following is valid in JML //@ ghost public ensures invariant;,
   ghost switches the lexer mode, and public is still a keyword signaling a modifier in the expr (inner) mode. In contrast, //@ ghost helper ensures invariant; would throw an exception, although helper is a modifier, because the lexer mode switch forces to emit helper as an identifier.

   The JML syntax is normally <modifier> <construct keyword> .... The construct keywords are keywords that force a specific JML construct, like invariant, initially, and normal_behavior.

   This is not true for model methods or field declaration. We promote ghost/model from an arbitrary modifier to construct-keyword that introduces ghost or model elements.

   Hence, ghost public int x will be invalid, as invariant public int x is invalid.

[wadoon]

Backtick-escaping is added. Following is valid:

//@ model `model` `model`(`ghost` `ghost`) { return `ghost`; }

[mattulbrich]

Thanks! I'd like to keep this open for discussion for a moment.

I must admit that apart from technical necessity, model `model` `ensures`; reads a lot better than blindly using model/ensures as identifiers here.

This very backticking mechanism is used in mysql, Kotlin and Scala; so we are in good company.