Quantifiers in Java

[Sophie Lathouwers]

Hi everyone,

I'm having some trouble with the correct syntax/use of quantifiers in a Java program. I am trying to verify the following program (originally an OpenJML example https://www.openjml.org/examples/max-by-elimination.html), I have made the text bold where I'm struggling with the syntax:
public class MaxByElimination {

  public static int max(int[] a)
  //@ requires a != null &*& array_slice(a, 0, a.length, ?vs) &*& a.length > 0;
  //@ ensures a != null &*& array_slice(a, 0, a.length, vs) &*& 0 <= result &*& result < a.length &*& forall_(int i; 0 > i || i >= a.length || nth(i, vs) <= nth(result, vs));
  {
    int x = 0;
    int y = a.length-1;

    while (x != y)
    /*@ invariant a != null &*& array_slice(a, 0, a.length, vs) &*&
                  0 <= x &*& x <= y &*& y < a.length &*&
                  (
                    (
                      forall_(int i; 0 > i || i >= x || nth(i, vs) <= nth(y, vs)) &&
                      forall_(int i; y >= i || i >= a.length || nth(i, vs) <= nth(y, vs))
                    ) || (
                      forall_(int i; 0 > i || i >= x || nth(i, vs) <= nth(x, vs)) &&
                      forall_(int i; y >= i || i >= a.length || nth(i, vs) <= nth(x, vs))
                    )
                  );
    @*/
    //@ decreases y-x;
    {
      if (a[x] <= a[y]) x++;
      else y--;
    }
    return x;
  }
}

Trying to verify this results in an "Expression form not allowed here".
I have tried to stick to the way foralls were used in this example: https://github.com/verifast/verifast/blob/fe877962288c27c3ed487bf8781ffac9699f87c9/examples/forall.c
There were some examples with foralls in Java, but those used the forall to say something about all elements (all elements were not null) instead of about a range of the elements.

What would be the correct way to write a forall for a Java program?

Kind regards,
Sophie Lathouwers

[Bart Jacobs]

Hi Sophie,

VeriFast currently supports the forall_ construct only at the assertion level, not inside boolean expressions. So it does not currently support them in a disjunction or a regular conjunction. One way to write your invariant would be as follows:

... &*& exists<bool>(?b) &*& b ? forall_(...) &*& forall_(...) : forall_(...) &*& forall_(...)

Replacing the P || Q by exists<bool>(?b) &*& b ? P : Q means that you have to manually say which disjunct holds by closing an exists<bool> chunk.

This predicate is defined as follows:

predicate exists<t>(t x) = true;

Best,
Bart

--
You received this message because you are subscribed to the Google Groups "VeriFast" group.
To unsubscribe from this group and stop receiving emails from it, send an email to verifast+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/verifast/ea9389df-933c-47ca-b2ad-5cc5249a978bn%40googlegroups.com.

[Bart Jacobs]

This verifies:

public class MaxByElimination {

  public static int max(int[] a)
  //@ requires a != null &*& array_slice(a, 0, a.length, ?vs) &*& a.length > 0;
  //@ ensures a != null &*& array_slice(a, 0, a.length, vs) &*& 0 <= result &*& result < a.length &*& forall_(int i; 0 > i || i >= a.length || nth(i, vs) <= nth(result, vs));
  {
    int x = 0;
    int y = a.length-1;

    //@ close exists(false);

    while (x != y)
    /*@ invariant a != null &*& array_slice(a, 0, a.length, vs) &*&
                  0 <= x &*& x <= y &*& y < a.length &*&

                  exists<boolean>(?y_is_max) &*& y_is_max ?
                    (
                      forall_(int i; 0 > i || i >= x || nth(i, vs) <= nth(y, vs)) &*&

                      forall_(int i; y >= i || i >= a.length || nth(i, vs) <= nth(y, vs))
                    ) : (

                      forall_(int i; 0 > i || i >= x || nth(i, vs) <= nth(x, vs)) &*&

                      forall_(int i; y >= i || i >= a.length || nth(i, vs) <= nth(x, vs))
                    )

                  ;
    @*/
    //@ decreases y-x;
    {
      //@ open exists(_);
      if (a[x] <= a[y]) {
        //@ close exists(true);
        x++;
      } else {
        //@ close exists(false);
        y--;
      }
    }
    return x;
  }
}

To view this discussion on the web visit https://groups.google.com/d/msgid/verifast/ed8db458-0c24-5231-26b5-b5f5da0c6c4f%40kuleuven.be.