Support for JML `TYPE`

[flo2702]

KeY should have more support for the JML type TYPE.

As far as I know, KeY only supports the \type construct in expressions of the exact form \typeof(e) == \type(C). It does not understand the type TYPE and the operator <: at all.

Use case 1

Consider a class hierarchy like the following:

class A {
    //@ ghost TYPE packed;
    //@ invariant packed <: \type(A) ==> P;
}

class B extends A {
    //@ invariant packed <: \type(B) ==> Q;

    //@ requires this.packed == \type(B);
    //@ ensures P;
    //@ ensures Q;
    void foo() {}
}

The method contract of foo() should be provable.

Use case 2

Remembering the type of objects in a \seq or container object.

[mattulbrich]

I think this is easily achievable in KeY.

All we need is a sort SORT in KeY and a sort-depending symbol alpha::sort, a few taclets that connect them to the subtype relation of the Java program and JavaDL.

The JML translation is probably easily adapted.

A topic for the HacKeYthon?

[wadoon]

Does this hurt the theory on the meta-level?

• What is \type(\type(a))?
• Is \type only defined for reference datatypes?
• Is \type(2) well-defined? Or is\type(2)` a reference type due to autoboxing?
• Is \TYPE <: \TYPE?
• Is x <: y similar to instanceOf? Then, will it support annotations?

[flo2702]

\type(\TYPE) <: \type(\TYPE) holds.

\type is defined for type names. I.e., \type(ClassName), \type(int), and \type(\TYPE) are all legal expressions, but \type(\type(...)) and \type(2) are not.

The subtype operator supports only base types without annotations.

[flo2702]

Closed by #3465