Mattias Ulbrich
Mattias Ulbrich
Or take the method's assignable clause as a default like a number of other tools do. It is a good default.
While the title says this PR introduces new alias names, it seems that it changes the default keyword. I am not sure we all agree on doing that ...
It seemed to me that you renamed a few things from "assignable" to "modifiable", also in error messages. That led me to the conclusion that "modifiable" is the new default...
There are a number of fundamental questions to be sorted out: https://github.com/KeYProject/key/wiki/Polymorphic-types-in-KeY
Discussion at Hackeython: * Comparison with Scala's type system: All ADT definitions in our sense must be covariant (or invariant), cannot be contravariant. * We do not want to specify...
Nice issue number btw :smile:
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....
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?
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...
Interesting observation! Thanks for reporting. However, the problem is not SMT-related, but has to do with the fact that a local program variable `length` is created in the proof obligation...