Redundant assertions and `hence_by`

[flo2702]

The current JML reference manual includes redundant versions of most clauses. E.g., requires_redundantly x; means that x follows from the non-redundant requires clauses.

The reference manual has the following to say about assert_redundantly clauses specifically: "The assert-redundantly-statement must appear in an annotation. It has the same semantics as the JML form of an assert statement, but is marked as redundant. Thus it would be used to call attention to some property, but need not be checked." It says nothing about assume_redundantly.

In addition to assert_redundantly, there are also hence_by, and (very confusingly) hence_by_redundantly: "The hence_by statement is used to record reasoning when writing a proof by intermittent assertions. It would normally be used between two assert statements or between two assume statements." There is one example of such a statement on pp. 110--111:

//@ assert i < 0 && -1 <= i && i <= a.length;
//@ hence_by (i < 0 && -1 <= i) ==> i == -1;
//@ assert i == -1 && i <= a.length;
//@ assert sum == (\sum int j; 0 <= j && j < a.length; (\bigint)a[j]);

There are several questions that arise from this:

1. According to the categorization in #28, hence_by would be a prover guidance statement rather that a specification element. Since the exact way such prover guidance works differs greatly between tools (e.g., I think in KeY, we may prefer to have something like //! hence_by <rewrite_rule> instead of //@ hence_by <jml_clause>), I think it's best to remove this from the standard.
2. The semantics of assert_redundantly quoted above don't make sense to me. What is the point of an assertion if it does not have to be checked? I suggest the following instead, which would put assert_redundantly in line with other redundant clauses: "An assert_redundantly statement is only allowed to occur after a series of assert statements. The statement must follow from the assert statements above it, without taking into account the surrounding context."
3. What are the semantics of hence_by_redundantly? I cannot make any sense of this.

[davidcok]

In #24, hence_by was agreed to be deprecated. assume can fill the same function -- providing a lemma.

[mattulbrich]

I wonder if assume really introduces a lemma or not rather an axiom since there is no justification for the lemma.

[mattulbrich]

One could read the phrase in the refman as: "The redundant assertion might be verified statically as redundant such that a runtime inspection does not make any sense." Itshould be made clearer though.

[davidcok]

It was agreed earlier to deprecate hence_by but to keep the various forms of _redundantly (given arguments from Gary). OpenJML currently treats constructs with _redundantly precisely the same as their non-redundant counterparts. However, per the DRM, given

requires P;
requires_redundantly Q;

One ought to be able to (and be required to) prove P ==> Q

Similarly there are proof obligations stemming from the implies_that and for_example sections (that OpenJML does not implement).

[davidcok]

My current understanding of this issue is that the _redundantly, implies_that and for_example features remain as non-core JML features, but that their proof obligations remain to be documented.

[leavens]

Mattias wrote:

One could read the phrase in the refman as: "The redundant assertion might be verified statically as redundant such that a runtime inspection does not make any sense." It should be made clearer though. Yes, I agree. The intent of the paper

Gary T. Leavens and Albert L. Baker, "Enhancing the Pre- and Postcondition Technique for More Expressive Specifications", in (Jeannette M. Wing and Jim Woodcock and Jim Davies (eds.), FM'99 --- Formal Methods: World Congress on Formal Methods in the Development of Computing Systems Toulouse, France, September 1999, Proceedings, Springer-Verlag, LNCS Vol. 1709, pp. 1087-1106, 1999, http://dx.doi.org/10.1007/3-540-48118-4_8 .

is to allow one to be explicit about what is redundant, and thus allow such redundant clauses to be checked. In all cases there is some implication that could be checked in logic (usually that the non-redundant clause implies the redundant one). I agree that these redundant clauses are very seldom if ever used, and that their proof obligations should be documented if kept in JML.

The hence_by statement was intended to document in-line proofs of programs that use intermediate assertions in calculational style. We already agreed to remove it along with hence_by_redundantly (which I agree was overkill, in hindsight). So there is no point in discussing it further...

(gratuitous aside) Still, I wanted to say that the original idea of hence_by was that one could write something like:

assert x >= \old(x+1);
hence_by (x >= \old(x+1)) ==> (x > \old(x));
assert x > \old(x);

so that the expression following hence_by should be always true. However, in calculational style proofs one would usually write "predicate calculus" instead of such a formula, so this isn't that helpful. And I can't imagine why one would really want to use hence_by_redundantly, it was just excess regularity in the design. In any case, we agreed to get rid of hence_by. (end gratuitous aside)

[mattulbrich]

With labelled clauses, how about a tool specific extension like:

//@ assert gt_plus1: x >= \old(x+1);
//@ assert gt: x > \old(x);  //+KeY@ \using gt_plus1;

If it will be needed in a tool it will be added as a tool-specific instruction, I am sure.

[davidcok]

Such a use is fine with me. In fact, OpenJML also has a mechanism to apply rewrite lemmas, needed in situations where some conversion between bit-vector expressions and integer expressions is needed (which SMT does not do well).

[davidcok]

Just a coda here about how I use lemmas in OpenJML.

One example:

//@ ensures \result == (mod(k,1) == (k&1));
//@ public static pure model odd(int n) { returns true; }

void m() {
  ...
  //@ assume odd(101);
  ...
}

The odd method gets proved if it can, and then a particular instantiation can be assumed in the middle of some other code, providing a lemma there to help a proof along. This does not require anything beyond current JML capabilities, though it occurs to me that the assume here is a good candidate for hence_by. Remember the the postcondition of the callee is assumed here, providing just the effect we want. Preconditions can be checked and enforced as well, though there are none here.

Another pattern for the same effect is

//@ ensures mod(k,1) == (k&1);
//@ public static pure model odd(int n) {  }

void m() {
  ...
  //@ set odd(101);  -- or //@ use odd(101);
  ...
}

Here I added the use keyword to allow putting in a method call. Again the postcondition of the callee is assumed at the call site. This is a bit more obvious and another candidate for using the hence_by synonym for assume.

I think both of these uses are similar to what Mattias means by \using (which, by the way, would be an illegal unicode sequence).

[mattulbrich]

Good point.

I am reluctant to use the former concept because assume is a dangerous and potentially evil construct. A student has introduced lemmas in a similar way, but via //@ assert odd(101);. Since KeY can expand the method body, the assertion is trivial, but one still gains the postcondition.

I favor the second form by far. Have used it many times. Usually not via model methods but via actual Java methods (which is admittedly less elegant). The reason for not using model methods is the lack of a //@ use statement. Is that JML? I would love to have something like this in KeY. ... It would fall into the proof control category however. //@ set odd(101); reads strange. I had always thought about //@ call odd(101); but that is not really what it is about, I seem to like use better.

[mattulbrich]

I think both of these uses are similar to what Mattias means by \using (which, by the way, would be an illegal unicode sequence).

That \unicode business is annoying, but thank, David, well-spotted.

I would expect to have more internal things behind a "using" clause. It would perhaps read

assert \dl_seqPerm(a, b) \using "rule seqPermSym x=a y=b; rule seqTrans on='seqPerm(b,c)'; auto local";

(which is a fictive script in our real scripting language in KeY) Now this is really low level proof control, but I think there are cases where you need to go down to the engine room.