Printing JML for quantifiers with multiple variables

[samysweb]

This is either a parsing bug in KeY or a printing bug in JML Parser. Given the file

public class PolishFlagSort {
    /*@
      @ public normal_behavior
      @    ensures (\forall int I, J; 0 <= I && I < J && J < ar.length; ar[I] <= ar[J]);
      @*/
    public static void sort ( int[] ar ) {
    return;
    }
}

reprinting via JML Parser produces:

public class PolishFlagSort {
    /*@  normal_behavior
        ensures (\forall int I, int J;0 <= I && I < J && J < ar.length; ar[I] <= ar[J]);
        */
    public static void sort(int[] ar) {
        return;
    }
}

Note the , int J vs , J.

This is not blocking our project so no hurry, but I wanted to persist this observation. From a superficial glance this does not seem to be fixable quickly.

[WolframPfeifer]

I looked it up in the grammar (https://github.com/KeYProject/key/blob/51f368c9ee0da2d2e053933de19e202ef7f36af4/key.core/src/main/antlr4/JmlParser.g4#L387): The JML parser of KeY allows the declaration of multiple variables with a single quantifier. However, these variables all must be of the same type, so the printed contract is not valid KeY-JML.

Btw., I noticed that the visibility modifier public is missing from the printed contract ...