Support OpenJML for Arbitraries

[jlink]

Testing Problem

It should be possible to create arbitraries from (a subset of) OpenJML specifications.

The most simple example (taken from https://www.openjml.org/examples/sum-max.html):

 //@ requires a.length > 0;
  void max(int[] a) {
    int sum = 0;
    int max = a[0];

    //@ loop_invariant 0 <= i <= a.length;
    //@ loop_invariant sum <= \count * max;  // Assertion to be proved
    for (int i=0; i<a.length; i++) {
      //@ assume Integer.MIN_VALUE <= sum + a[i] <= Integer.MAX_VALUE; // Just assume we never overflow
      sum += a[i];
      if (max < a[i]) max = a[i];
    }
  }

Referencing this method should enable jqwik to use Arbitraries.integers().toArray().withMinLength(1) for running properties on max(..).