Soundness: Invariants, model methods and model fields need not be well-founded

[mattulbrich]

Description

Expressions in invariants, model field represents clauses and bodies of model method need not be well-founded.

While for a Java method this corresponds to a partial proof (termination not shown), for a an axiom like the above definitions, ignoring to prove well-foundedness may introduce inconsistency.

As an example, consider the model method

model int f(x) { return f(x)+1; }

which would introduce an axiom of the shape

\forall int x; f(x) = f(x)+1

which is equivalent to false.

There is a setting in KeY to check recursive definitions, but this is already incomplete, and the situation is worse than explained in the disclaimer of the option modelFields where it says that cross-definitions may still occur.

The present example exploits that one can express something like

//@ invariant ! \invariant_for(this);

which is of course contradictory in itself.

We do need to introduce well-foundedness checks.

Reproducible

always

Steps to reproduce

Load the attached proof bundle to find proofs for the following class:

final class A {

    A next;

    //@ invariant !\invariant_for(next);

    //@ normal_behaviour
    //@  ensures next == this;
    A() {
        next = this;
    }

    //@ normal_behaviour
    //@  ensures false;
    static void ohDear() {
        A a = new A();
    }

}

---

• Commit: 470b0d6

[mattulbrich]

There is an alarmingly similar issue #592.