A new category of JML items

[mattulbrich]

I'd like to suggest to distinguish between different types of JML annotations:

1. top-level specifications. Contracts (behaviours), static and instance invariants, model fields/methods, ghost fields,
2. auxiliary specifications. Assertions, assumptions, loop specs, block contracts, (perhaps helper contracts also)
3. prover guidance statements. (Assertions), proof scripts, debug, show, contract choice, ...

The first category is why we are here: These are the properties we'd like to guarantee to the world.

The second category has its specification and documentation value of its own, but is actually required to modularly divide-and-conquer the proof obligations.

The third category is actually not specification at all. It is interaction with the verifier tool and needed to make proof go through or to debug them.

Most existing JML commands fall into 1 and 2.

I wonder if the third category should not be made different from specifications more clearly. In KeY we had the discussion that we would not start such prover guidance steps with //@ but with another sequence like //!. Thus, it becomes immediately clear, what is specification, and what is prover interaction.

On a side branch in KeY, //! can be used for proof scripts. We plan to advance this to choice of (named) contracts. There is one command //@ merge_point for controlling flow interaction with symbolic execution.

One should quickly be able to read a JML-annotated method and notice the Openjml- or KeY-prover guidance commands and just ignore them.

Indeed, I'd suggest: We have a different annotation prefix or another special easy-to-see identification for prover guidance commands that are not specification elements.

Suggestions include:

• '//!'
• commands start with underscore: _show, _merge_point
• prefix commands with a special keyword like //@ guide show. or "prover". or "do". or ...

[dmzimmerman]

I seem to remember a discussion, perhaps at Dagstuhl, perhaps at Shonan, about something similar to this (there were prefixes //@+, //@- or something to that effect), where you would have different annotation indicators for annotations that were there to support specific tools. I don't, however, remember offhand what the outcome of that discussion was at the time.

I don't know that I'd refer to (2) as auxiliary, since as you say, they're pretty essential (e.g., you're generally not going to prove anything useful about a method with any non-trivial loop in it without loop contracts). Perhaps internal or similar?

[mattulbrich]

Yes, Dan, we were discussing these tool-specific prefixes e.g. on #3. The are/will be part of the language definition.

I thought auxiliary was the coined notion for such clauses, but I would be happy to rephrase that.

[leavens]

I'm okay with having tools understand //! (and also /! ... /) comments to be tool annotations, along with the other conventions suggested.

[davidcok]

I see categories 2&3 containing all constructs that are placed within the body of a method, plus perhaps axiom, whereas cat 1 is everything declared in a type body or method spec.

To me the difference between categories 2 and 3 is blurry. All the category 2 constructs are there to assist proofs. Even loop specifications would be omitted if there were means to infer loop specs. assume statements just help proofs where the prover is not able to establish some axiom/lemma for itself. assert serves as a lemma or debugging tool.

So I think the beneficial distinction is between proof assistance/internal specification documentation constructs that are so commonly used and valuable that all tools should implement them the same way (cat 2) and (cat 3) those that are not sufficiently useful or agreed on to be standardized. But I thought we were leaving this last category out altogether.

If so then they should be in a category of tool-specific constructs -- and those are accommodated by //+KEY@ and //+OPENJML@ and the like. If we use something like //! (across all tools) then all tools have to be able to parse them and sort out which //! comments it know about and which it does not. We want users to be able to specify and markup (with proof assistance) commands and apply various tools without having to have wholly different copies of source code for each tool.

On the other hand if we think there are useful and so standardizable constructs in cat 3 and we want to distinguish them from cat 2, we could use a different prefix. But I would advocate either just putting them in category 2, or still having a root prefix of @, such as //@!

[leavens]

The comments by David (@davidcok) seem sensible to me.

However, if there are proof-aids that are tool-specific, won't we need to have different tools understand different ones?

[mattulbrich]

I see your point. But ...

I feels different to write //@ apply tool_magic_42; rather than //@ assert something;. There is a felt conceptional difference.

[wadoon]

I think there is a different between proof-aids and tool-specific instruction: the language.

For example, loop invariants are defined by JML and uses JML syntax, but tool-specific commands does not need to follow the JML syntax style. KeY would use JavaDL rather than JML for the notation formulas, and KeY commands look more like a Shell commands rather than Java.

So keeping them separately seems a good idea, so we decided on //! in KeY.

On the other side, if we decide on common proof-aids which also follow the JML syntax, I am willing to accept them in JML annotation texts, ie., //@ or /*@.