Help for using the existence of an array that fulfills a condition.

[fab918]

For a more complex example, I need to test whether an array exists that satisfies a condition.

I've created an artificial example using the 2 methods I've found to run these kind of tests, however, it doesn't work and I can't find why.

The example is deliberately artificial.

• Could someone help me get these examples (which use an array with certain conditions) to work?

• Is there a better syntax?

    //@ requires value >= 0 && value <= 10;
    //@ requires size >= 0;
    //@ ensures \result == true ==> (\exists int[] arr; arr.length == 10;
    //@ (\forall int i; 0 <= i && i < arr.length; arr[i] == value) &&
    //@ (\sum int i; 0 <= i && i < arr.length; arr[i]) > size);
    public static boolean test(int value, int size) {

        return value * 10 > size;
    }

    //@ public static model int[] arr;
    //@ requires value >= 0 && value <= 10;
    //@ requires size >= 0;
    //@ ensures \result == true ==> (arr.length == 10 &&
    //@ (\forall int i; 0 <= i && i < arr.length; arr[i] == value) &&
    //@ (\sum int i; 0 <= i && i < arr.length; arr[i]) > size);
    public static boolean test(int value, int size) {

        return value * 10 > size;
    }

[Loewensenf]

The actual method body simply checks if value * 10 > size without explicitly creating or manipulating an array.
This may disconnect the specifications and the method body and causes the issue. Specifically, KeY might have trouble inferring the existence and state of an array solely from the postconditions without any explicit array handling in the method body