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.
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.