Missing? rules for class invariants

[BookWood7th]

When trying to prove a small example, I noticed that the Static_class_invariant_axiom_for_A rule is only generated when trying to prove method contracts in A. When I tried to prove B#b(), there was only a partial invariant axiom rule, which did not allow me to close the Precondition branch for the method contract of A#m()

class A {
    //@ public static invariant true;

    //@public normal_behavior
    //@ensures true;
    public static void m() {
    }
}

class B {
    //@normal_behavior
    //@ensures true;
    public void b() {
        A.m();
    }
}

Why does KeY not generate a rule to unfold the invariants of A?

[WolframPfeifer]

I am not sure if I understand the problem from the description. You need to prove (in JML terms) \static_invariant_for(A) when calling A.m(), but are not able to unroll its definition? If that is the problem, I agree that there should be a rule to unroll the definition, since there is no dynamic binding involved and the exact invariant should be known.

Another approach (maybe how it is meant to be used?) would be to require \static_invariant_for(A) in the precondition of b. This way you don't need to know the definition.

The partial invariant rules should not be related at all as far as I know, since they are for the non-static case. These are needed when the type of an object x is not exactly known (since it could also be of a subclass), and you cannot replace x.$inv() on the sequent by the definition, but only unroll it partially in the antecedent.

[BookWood7th]

Yes, that is correct. I would need to prove "\static_invariant_for(A)", but cannot unroll it.

Requiring that the static invariant holds would prevent me from proving any method that modifies the heap first before calling A.m(). Even if this heap change would be unrelated.

[WolframPfeifer]

We just discussed this in our developer meeting. It seems to be an implementation restriction (we don't want to have too many rules to prevent slow down of the taclet matching engine), there should be no conceptional restriction that forbids to unroll.