Enable class invariants for all classes.

[mattulbrich]

Invariants can only be extended for the local class or all final classes and there is no good reason for this restriction. Hence we suggest to lift this restriction.

Underlying problem

In reality, knowing about invariants should not be limited to final classes. The generated taclets are guarded by an exactInstance expression making the scenario sound.

The restriction seems rather arbitrary.

Estimated effort

Well, it seems the 3 lines below could easily be removed.

... We should just think about it to make sure it is sound and does not compromise automation.

Additional context

key/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java

Lines 1049 to 1052 in ae75e81

	for (KeYJavaType kjt : services.getJavaInfo().getAllKeYJavaTypes()) {
	if (kjt != selfKjt && !ji.isFinal(kjt)) {
	continue; // only final classes
	}

[mattulbrich]

#3583 is needed to be able to experiment with this ...

[mattulbrich]

Reported by Fabian Koffer in the BSc thesis.

[WolframPfeifer]

Isn't that what the Partial_inv_axiom_... taclets are for? As far as I know, you cannot "unroll" the exact definition of the invariant for non-final classes (i.e. replace o.<inv> on the sequent), since it could be refined in a subclass. Therefore, it is possible to add all the clauses from the superclass (individually) via Partial_inv_axiom_.... Am I missing something?

[mattulbrich]

As far as I know, you cannot "unroll" the exact definition of the invariant for non-final classes

You can unroll since the definition axioms have C::exactInstance(o) as a precondition and are hence sound also for non-final classes.

[mattulbrich]

In our discussion we found out: We want to have these taclets for final and non-final classes, but not for abstract classes and interfaces. The reason is that these do not have extInstances anyway.