Missing rule for type of array

[WolframPfeifer]

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 implies F[]::exactInstance(x) = TRUE. For implementing this, we probably need an additional Varcond isFinal or similar.

Reproducible

always

Steps to reproduce

1. Load a .key file with the following content:

   \programVariables {
       int[] x;
   }
   
   \problem {
       int[]::instance(x) = TRUE
       ->
       int[]::exactInstance(x) = TRUE
   }
   
   

This can not be closed in KeY.

[mattulbrich]

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.

[mattulbrich]

It seems that treating int[] as a final class would resolve the issue. Am I right? If so, perhaps one can mark such types as final?

[mattulbrich]

I wonder if that is a problem with arrays at all. If A is a final class then

A::instance(a) = TRUE, a != null ==> A::exactInstance(a) = TRUE

can also not be proved.

[WolframPfeifer]

Closed by #3543. Thanks, @mattulbrich!