Common Example‎ > ‎

ArrayMax in VeriFast

  • "The Java lemma library is smaller than the C lemma library, hence some additional lemmas were required."

/*@
fixpoint boolean forall<t>(list<t> vs, fixpoint(t, boolean) q) {
  switch(vs) {
    case nil: return true;
    case cons(h, t): return (q)(h) && forall(t, q);
  }
}

lemma void forall_append<t>(list<t> vs1, list<t> vs2, fixpoint(t, boolean) q) 
  requires forall(vs1, q) == true &*& forall(vs2, q) == true;
  ensures forall(append(vs1, vs2), q) == true;
{
  switch(vs1) {
    case nil:
    case cons(h, t): forall_append(t, vs2, q);
  }
}

lemma void increase_max(list<int> vs, int max, int max2)
  requires forall(vs, (geq)(unit, max)) && max <= max2;
  ensures forall(vs, (geq)(unit, max2)) == true;
{
  switch(vs) {
    case nil:
    case cons(h, t): increase_max(t, max, max2);
  }
}

fixpoint boolean geq(unit u, int x, int y) {
  switch(u) { case unit: return x >= y; }
}

lemma void take_one_more<t>(list<t> vs, int i)
  requires 0 <= i &*& i < length(vs);
  ensures take(i + 1, vs) == append(take(i, vs), cons(nth(i, vs), nil));
{
  switch(vs) {
    case nil:
    case cons(h, t):
      if(i == 0) {
      } else {
        take_one_more(t, i - 1);
      }
  }
}
@*/

class ArrayMax {
  static int arrayMax(int[] a)
    //@ requires a != null &*& array_slice(a, 0, a.length, ?vs);
    //@ ensures array_slice(a, 0, a.length, vs) &*& a.length == 0 ? result == 0 : mem(result, vs) == true && forall(vs, (geq)(unit, result));
  {
    if(a.length == 0) {
      return 0;
    }
    int max = a[0];
    //@ switch(vs) { case nil: case cons(h, t): }
    for(int i = 1; i < a.length; i++) 
      //@ invariant 1 <= i &*& i <= a.length &*& array_slice(a, 0, a.length, vs) &*& mem(max, vs) && forall(take(i, vs), (geq)(unit, max)); 
    {
      int ai = a[i];
      if(max < ai) {
        //@ increase_max(take(i, vs), max, ai);
        max = ai;
      }
      //@ mem_nth(i, vs);
      //@ take_one_more(vs, i);
      //@ forall_append(take(i, vs), cons(ai, nil), (geq)(unit, max));
    }
    return max;
  }
}

Comments