What should the specification comment syntax be?

[pieter-bos]

I would like to pin down a grammar for specifications in comments. Some things to consider:

1. In what positions is @ allowed to start a specifications?
2. Are extra @ allowed, required, disallowed at the start of a new line?
3. Is one extra @ at the end of a block comment allowed, required, disallowed?
4. Are line comments disallowed or allowed in block comment specifications?
5. What if we want @ to be mandatory at every line - are line comments then disallowed?
6. What happens if a block comment is closed while within a line comment in the block comment?
7. Is it allowed to re-enter specification mode with an @ while in a line comment in a block comment?
8. If so, what happens if I close a block comment in a specification line comment in a specification block comment:

/*@ requires true; //@ requires false; */

[bobismijnnaam]

I always assumed the following uses were standard (not exhaustive):

1. Opening a block with /*@, possibly with whitespace inbetween the * and the @.
2. Ending with @ is optional.
3. The entire spec block comment can optionally be left-padded with @. On the left of the padding, only whitespace is allowed.

Personally, 4. I would like it to be possible to jump in and out of specs within comments, as that seems like a nice feature to have when you are prototyping. This means //@ requires true; // comment should parse, as should /*@ requires true; // first pre */.

Then, answering your points in order, with my points in mind:

1. After opening a comment, as long as you're typing whitespace. Once you stop typing whitespace you are in a regular comment. Once you type an @, you enter spec again.
2. Allowed, as long as you're typing whitespace.
3. Allowed.
4. Allowed.
5. IMHO we don't want that.
6. Nothing, you go back to plain "code" mode.
7. Yes, as long as there was only whitespace between the start of the line comment and the @
8. You go back to code mode. I see this as an obvious result of not having nested comments; am I missing some technicality here?

I made diagrams a while ago to visualize the comment state machine I was thinking of. I hoped that my above uses would induce a simple state machine, but of course it does not. I'm also not sure if it's complete or correct, but I guess it's a start towards being clearer about these rules. It implements the following ideas:

• Switching back and forth between spec mode and plain comment mode
• Line comments that can be either spec or plain, in block comments
• @ preceded with zero or more whitespace is interpreted as enabling spec mode

specification_comments_state_machine1.dot.txt

(For this diagram, reading the plain dot might be more informative than the diagram, as the dot is effectively a case distinction over states and inputs)

Some ideas we can apply to simplify:

• Break with JML tradition: we only resemble JML, so we shouldn't have to bend over backwards to support their idioms. This allows us to discard blocks with padding of @'s. Instead, only allow them as a marker at the start of the comment
• Do not allow nesting of spec line comments in plain block comments
• Do not allow switching of spec to plain to spec to ... etc. within line comments

Personally, I think applying all three of above ideas would result in a bit of a clunky to use specification language, but at least it would be easy to implement and explain, which are also nice characteristics to have.

If I could decide how to move forward, I would first have a vote in a vercors meeting on the above 3 and other concerns we can formulate concisely, and then go from there.

[bobismijnnaam]

Here's what I'd expect to get if we apply the 3 simplifications (with fix from Lukas):

specification_comments_state_machine2.dot.txt

Practical implications:

• @ only appears once when starting a comment line, directly after the //
• In spec lines you can leave spec via //, and you cannot go back
• In spec blocks, you can enter a comment line. There, you can close the block, or have a newline, which enters spec again.
• Closing a spec block with @ is optional.

Easy to explain, small and somewhat symmetric diagram, and I think it reflects mostly how we and students use vercors specs in java. But then again it might be too limiting...

I think if I could decide, this is what I would do. But breaking with JML that much might be a bit too much for VerCors in general?

[ArmborstL]

Note that in the first diagram, the [^\s@] in all cases should also include //, to properly parse e.g. // //@ requires true; (currently, the second // would trigger the [^\s@], and one would not end in the line spec state).
Also, moving from block spec back to undetermined with \n should be removed, as you called the extra @ left-padding optional.

In the second diagram, there should be an additional transition from block spec to plain block comment with /*.
Also, you disallowed whitespace between /* or // and @ when starting a spec. I'm not saying it's wrong, just that it's a change you did not explicitly mention. Personally, I think it may be confusing if /* @ does not get parsed as a spec, especially if the user uses a font where the space character is quite narrow.

[ArmborstL]

My two cents: I think I would prefer it to be quite flexible. So in particular:

1. Allow the @ to follow the comment start directly (like /*@), but also whitespace between (/* @). If there is other text between, then I probably would not consider it as a spec start (e.g. /* this issue was raised by user@example.com). I don't have a strong opinion on the case that there is text in between that ends in a new line (e.g. /* for newbies: this is a JML specification, checked by VerCors\n @ requires x>0;*/). In my example it makes sense, but it can also easily use a line comment instead (i.e. /*@ // for newbies: JML\n @ requires x>0;*/). Another thing to pay attention to is doc strings, which may have tags like @author. So probably @ cannot start a spec inside a doc string (i.e. /**-comments).
2. Allowed
3. Allowed
4. Allowed! Apart from commenting out specifications during development, it also allows comments explaining the spec.
5. N/A
6. I think that the java standard says that this ends the comment. So it would also end any kind of spec. In particular, it seems that javac considers the afterwards in /* block comment // nested line comment*/ afterwards to be outside any comment. But this specific case is indeed a bit iffy...
7. As mentioned in 1., I would not start a spec if there is non-whitespace text between the // and @. If we have a //@ within a block spec, I think both cases have their merit: It is normally a start of a spec, so it is the same here. Or it is a commented out spec (e.g. /*@ requires good();\n // @ requires broken();\n @ ensures goodResult();\n @*/). So I don't have a strong opinion on this case.
8. Given my considerations in 6., I would say it ends all comments and specs.

So I'm slightly less permissive than Bob (e.g. no line spec nested within line comments).
Regarding Bob's simplifications: I would keep the possibility of extra @ left-padding. The others, I can accept.

[bobismijnnaam]

Oof, doc strings are a good point. That feature breaks my ultra-permissive diagram above...

e.g. no line spec nested within line comments

How does this follow from your points 1 - 8?

Diagram of simplifications + padding with @ of both line and block comments:
specification_comments_state_machine3.dot.txt

[ArmborstL]

e.g. no line spec nested within line comments

How does this follow from your points 1 - 8?

I considered it as part of "If there is other text between, then I probably would not consider it as a spec start", because there is other text between the first // and the @. But it's true, I wasn't 100% clear on that point. So to be clear: I want no line spec nested within line comments 😉

Regarding your new diagram: linespec does not allow whitespace between // and @. I probably would allow spaces there.
Also, it should be possible to go from "@ padding" to "nested line comment".

[ArmborstL]

I like your updates. Some more changes 😜 :

• "plain line comment" should go back to "code" with a */
• "block undecided" should go back to "code" with a */

[bobismijnnaam]

Points made during the vercors meeting:

• The only use case of nested spec/plain comments is that of having a comment line inside a spec line/block. Other nestings, or toggling between plain and spec mode, is not necessary
• We aim for similarity with OpenJML for reuse. So whatever we decide, we should check if the behaviour is similar, and if the below claims hold.
• OpenJML only recognizes blocks that start with an @ directly after the comment marker. So only //@ and /*@ should be recognized
• OpenJML allows padding spec blocks with @ and whitespace before that, so we should allow that as well

This seems mostly in line with what the JML reference manual suggests (https://www.openjml.org/documentation/, sec. 4.1.3 - 4.1.9). What they have on top of that is the following: JML also allows toggling of modes, there's some business about having spec comments with keys to enable some specs only in some situations, and they define how spec expressions can span multiple line comments.

I think we should follow the JML spec up to the stuff vercors doesn't have currently, which is (correct me if I'm wrong) the toggling, specification keys, and having expressions span multiple lines. For all the other stuff we can take the JML manual as a specification.