New JML specification elements

[wadoon]

After a discussion with @WolframPfeifer, we would like to propose the following additions/changes to KeY JML:

1. invariant_free (on class level) is the same as axiom specified by the JML reference manual.
   axiom is indeed the better notion.

2. Introducing lemma <expr>; clause on class-level could be beneficial.
   The difference to axiom would be, that a lemma should be provable in the given theory and the class' axioms.

   Note, that different syntax discussion is open. We also discuss a more model-method style.

3. Also on class level, predicate clause //@ predicate P(x) = ary[x]+1>0 could help to write and read JML Specification.

We are aware that, (2) and (3) are already doable via model methods. We would also likely to implement these via model methods.

[mattulbrich]

Thanks for the initiative.

Ad 1. Agree. It is better to make it clear that there is a possibly unsound/inconsistent axiom in the system. But an invariant would only hold if the invariant of this was true whereas axioms are unconditional. I do not have application cases in mind, but they might differ. (An axiom can obviously be guarded by \invariant_for(this), so no loss of expressivity.

Ad 2. In most cases, a lemma needs some type of proof. (Why formulate it as a lemma otherwise?) How should proofs be presented? Dafny does so in code. lemma is a synonym for method there. Moreover, lemmata usually do not apply unconditionally and will be "invoked" at specific points in the program. How would that be done then? Model/ghost methods are naturally invoked.

There may be invariants that follow from other invariants. Could we use \invariant_redundantly in that case.Seems to be just the wanted thing.

Ad 3. Why not use a model method? I would not introduce yet another syntactical category. Yes, //@ model boolean P(x) { return ary[x]+1>0; } has a few more characters, but it explains itself. What about predicates when you override a class? Can they have contracts?