ghost label

[davidcok]

I forgot to include this item in the feature list. There is sometimes a need to add a ghost label in the body of a method as ghost code, as the target of an \old expression.

OpenJML implements this as //@ a:

But I could see requiring a statement: //@ a: ; or //@ a: {} Or one could require the keyword ghost as in other ghost code: //@ ghost a:

The current OpenJML solution fits if you are actually labelling another JML statement: //@ a: set x = ... is equivalent to //@ a: //@ set x = ...

Aside from requiring the lookahead to see the : so as to disambiguate the 'a' from a keyword, this is unproblematic grammatically.

I expect the ghost label would have the same categorization and \old with label, which is currently marked Core

[mattulbrich]

I like it better without the ghost.

[davidcok]

So @leavens, are you OK with //@ a: and with it being in the Core, along with \old with label?

[leavens]

Yes, I'm okay with using //@ label: for labels in JML annotations and making that core along with \old with a label argument.

[wadoon]

We should aware that //@ a: collides and share the syntax with #3.

[mattulbrich]

We should aware that //@ a: collides and share the syntax with #3.

I do not see this collision.

[wadoon]

We should aware that //@ a: collides and share the syntax with #3.

I do not see this collision.

The collision is described in "Suggestion (B)", where names are prefixes in the JML annotation texts.

[davidcok]

Closing this as consensus with the syntax //@ a: {} with the brace-pair optional if a Java statement follows.

[lks9]

We should aware that //@ a: collides and share the syntax with #3.

I do not see this collision.

The collision is described in "Suggestion (B)", where names are prefixes in the JML annotation texts.

Just for reference, this is in #18 and not #3.