Open WolframPfeifer opened 7 months ago
As a matter of fact, I think the above problem should not close as the lhs of the implication evaluates to to true for x=null
, but the rhs should not. Adding x != null
to the premise would repair that. It is still not provable then.
Description
The exact dynamic type of arrays of primitive values are always known. However, KeY is missing a rule here. There are also some real world cases, where the missing knowledge about the type on the sequent leads to unclosable goals.
For arrays of objects, it is not so easy, since there are subtypes of array types in Java. E.g., for a class A, A[] is a subtype of Object[].
However, for arrays of a final type F, we should have a rule that
F[]::instance(x) = TRUE
impliesF[]::exactInstance(x) = TRUE
. For implementing this, we probably need an additional Varcond isFinal or similar.Reproducible
always
Steps to reproduce
Load a .key file with the following content:
This can not be closed in KeY.