KeY loads the file without error message. However, in the sequent S does not occur anymore. Instead, "null" is printed.
The sequent looks like this:
Expected behavior
Some context on generic sorts (that was at least not completely clear to me before a discussion with @mattulbrich):
Generic sorts are placeholders that are to be instantiated with existing sorts "at verification time". They are allowed to appear in taclets (to express a family of rules), but not in the problem. The latter would result in a parameterized proof, which could be instantiated for concrete sorts (something that is possible in Isabelle for example, but not in KeY).
To avoid name clashes between the generic sorts and Java classes, the generic sorts are erased from the namespaces before starting the proof. It looks like this erasure happens before starting the proof (the resulting "null" probably stems from a toString() call where the sort object is null ...), but after parsing the problem. Thus, no error is thrown.
Additional information
The existing issues about generic sorts (#355, #720) seem to be outdated. It may be worth to investigate and close them if possible.
Description
If a generic sort is used inside a problem definition (in a .key file), this leads to a broken sequent.
Reproducible
always
Steps to reproduce
Load a .key file containing the following:
KeY loads the file without error message. However, in the sequent S does not occur anymore. Instead, "null" is printed. The sequent looks like this:
Expected behavior
Some context on generic sorts (that was at least not completely clear to me before a discussion with @mattulbrich): Generic sorts are placeholders that are to be instantiated with existing sorts "at verification time". They are allowed to appear in taclets (to express a family of rules), but not in the problem. The latter would result in a parameterized proof, which could be instantiated for concrete sorts (something that is possible in Isabelle for example, but not in KeY).
To avoid name clashes between the generic sorts and Java classes, the generic sorts are erased from the namespaces before starting the proof. It looks like this erasure happens before starting the proof (the resulting "null" probably stems from a toString() call where the sort object is null ...), but after parsing the problem. Thus, no error is thrown.
Additional information
The existing issues about generic sorts (#355, #720) seem to be outdated. It may be worth to investigate and close them if possible.