ghost and model declarations

[davidcok]

The only JML constructs that do not begin with a JML keyword are ghost and model declarations. I'd like to propose the (backwards incompatible) rule that for such declarations the ghost or model modifier must come first. This would greatly simplify parsing/error detection. Here is an example

public /*@ nullable */ static final Object o; // OK
public /*@ nullable */ static final /*@ ghost Object o; */ not OK -- must have the entire declaration including modifiers in JML

It is worse for methods where there are more modifiers JML modifiers that can apply to a Java method.

I also think it makes for a cleaner language design. Essentially, model and ghost would no longer be 'modifiers' but would be keywords introducing a declaration.

(Edited by @mattulbrich to make the * * not engage italic mode)

[wadoon]

I also thought about it during the holidays. I think the circumstance was that //@ ensures A; is ambiguous in JML, because it could be seen as a field A of type ensures or as a contract. A fixed mandatory keyword would help.

But as long as model and ghost are valid JML modifier for methods, I do not see any benefits for my generated parser. We need a rule that eliminates ghost and model as a modifier and is valid for both constructs: fields and method decls. I would rather propose:

model and ghost can only appear as the last modifier.

By this definition, I could eliminate them from the list of modifiers and they become mandatory construct-introducing keywords. This also brings both keywords in alignment with other JML constructs, e.g,

//@ public instance invariant = true;

The general rule for an JML construct is:

<Modifiers> {invariant|represents|accessible|...} 

[mattulbrich]

I'd also favour to not to have to write:

ghost public int x;

I think visibility should go first, also for specification stuff.

In the initial example: Can we not say that for ghost/model declaration, all modifiers must be in JML comments? whenever ghost is parsed after non-jml modifiers, the program is broken.

[davidcok]

I'll withdraw this idea as a late night intemperate frustration. Other constructs are also preceded by modifiers and the rule about JML constructs not using modifiers declared in Java means that for all of these it needs to be checked that no modifiers are leaking from Java into JML. That is one needs to distinguish public //@ normal_behavior -- illegal from //@ public normal_behavior -- OK and similarly for every other construct

[davidcok]

Regarding: In the initial example: Can we not say that for ghost/model declaration, all modifiers must be in JML comments? whenever ghost is parsed after non-jml modifiers, the program is broken.

That rule is indeed already the case. It is just a (admittedly doable) pain to check.

[wadoon]

Strangely, for my parser this is not a problem.

public /*@ghost*/ int T foo; //A

//@ public ghost int T foo;  //B

Both construct will be treated identical. In general, I would say form (A) is a grammar artifact that I raised by the fact that model and ghost are modifier (allowed for class, fields and methods). I would strictly discourage this form, because it makes the ghost variable accessible in Java scopes.

My proposal would eliminate this, as ghost and model are the last mandatory "modifier". The grammar rule would look as, for model/ghost methods:

<modifier> ['ghost'|'model'] <typeparam> <type> <name> '(' <args> ')' 
( <blockstmt> |  ';' )

[mattulbrich]

I suggest that the order of modifiers is not constrained and that all modifiers for a JML declaration must be in JML comments.

What problem would your proposal eliminate? (A) is illegal anyway.

[davidcok]

Form A is illegal JML. In OpenJML, any declaration that has ghost or model is checked to be sure that the whole declaration is in JML.

I have to add the checks that all of the modifiers are also in JML. It is somewhat difficult to reflect this in the grammar per se (and if you did it would make error recovery and messages more difficult, I expect)

[wadoon]

In my parser following resolve relative simple:

public //@ normal_behavior ensures true 
void foo(); 

The Java pass sees

KEYWORD(public) 
JMLDOC(//@ normal_behavior ensures true;) 
KEYWORD(void)
IDENT(foo)
LPAREN
RPAREN
SEMI

And in the JML pass I look into the JMLDOC tokens. In this case this results into an error, because at this position, only modifiers are allowed in JML/JMLDOC.

I think there is a simple rule in JML parsing: A Java construct can never associated to JML construct. Hence, the public in public //@ invariant true; does not refer to the JML comment, but to the Java construct following the comment. Therefore, all modifiers of a JML construct have to be in JML.

[wadoon]

But the case is not so easy, as JML modifier can refer Java constructs.

Would you allow the following syntax?

private //@ public
/*@ nullable */ 
/*@ normal_behavior ensures true;
void foo() {} 

In my parser/mind set this is ill-positioned: The contract is not allowed at this place. This is decided by the first Java modifier private.

Following is more difficult:

//@ public
/*@ nullable */ 
/*@ normal_behavior ensures true;
void foo() {} 

In my parser, public and nullable are modifiers for the contract. Only JML modifiers directly before Java decls are assigned to Java.

[mattulbrich]

|//@ public /@ nullable / /*@ normal_behavior ensures true; void foo() {} |

In my parser, |public| and |nullable| are modifiers for the contract. Only JML modifiers directly before Java decls are assigned to Java.

Is "nullable" a modifier of the method? One could argue it is a modifier for the return type and most be in front of the return type. I understood it this way.

[wadoon]

In this case, the nullable is a modifier of the contract (This is not allowed on contracts).

If nullable is put behind the contract, it is a method modifier. There is no possible way to have modifiers exclusively for return types of methods. It will always be ambiguous.

[davidcok]

Mattias is right on this point: as of Java 8, nullable and non_null; are type annotations, and are permitted on most uses of a (reference) type name

[wadoon]

There are no nullable or non_null modifiers in Java. There exists libraries, that provide Java annotations with a meaning of nullable/non_null references.

But modifiers are not annotations, and return types have no modifiers in Java. We should keep it this way.

The world of annotations is far more complex:

Syntax: All annotations are associated to the declaration! In public abstract @A R foo();, @A belongs to the method declaration.

Semantics: An annotation is applicable to certain elements (@TargetType annotation). If it is applicable to declarations, it is associated to the declaration, and if it is applicable to types, it is also associated to the return type.

Please refer to JLS 9.7.4 for more details. There is also the "closest type principle".

[davidcok]

JML has already made an equivalence between nullable and @Nullable etc. From Java 8 and beyond I think JML has no option but to consider @NonNull and non_null and @Nullable and nullable to apply to types.