is it allowed to assign a JML expression containing a quantifier to a ghost variable?

[waynee95]

Not sure if this is an actual bug or if I am missing something but I want to declare the following ghost variable:

        //@ ghost boolean containsValue = (\exists int i; 0 <= i < sortedArray.length; sortedArray[i] == value);

However, KeY won't let me do that. Instead I get a parser error.

[wadoon]

In the current version of KeY, but it is valid JML. KeY's parsing architecture sends this assignment to a javaparser that is only extended for a few simple JML expressions (excl. quantifier).

With #3195, a delayed parsing architecture should come, that avoids the javaparser.