Experiments with Encoding of the Next State Relations of Imperative Programs

// COST Verification Competition, Challenge 1: Maximum in an array
// http://foveoos2011.cost-ic0701.org/verification-competition

// Source: https://github.com/Microsoft/dafny/blob/master/Test/dafny2/COST-verif-comp-2011-1-MaxArray.dfy

var a: [int] int;
var n: int;

procedure main() returns (x: int)
  requires n > 0;
  ensures 0 <= x && x < n;
  ensures (forall i: int :: 0 <= i && i < n ==> a[i] <= a[x]);
{
  var y: int;
  /*ghost*/ var m: int;

  x := 0;
  y := n - 1;
  m := y;

  while (x != y)
    invariant 0 <= x && x <= y && y < n;
    invariant m == x || m == y;
    invariant (forall i: int :: 0 <= i && i < x ==> a[i] <= a[m]);
    invariant (forall i: int :: y <  i && i < n ==> a[i] <= a[m]);
  {
    if (a[x] <= a[y]) {
      x := x + 1;
      m := y;
    } else {
      y := y - 1;
      m := x;
    }
  }
}

var a: [int] int;
var n: int;

var y: int;
/*ghost*/ var m: int;
var x: int;
var bad: bool;

procedure main()
  modifies x, y, m, bad;
  requires n > 0;
  requires 0 <= x && x <= y && y < n;
  requires m == x || m == y;
  requires (forall i: int :: 0 <= i && i < x ==> a[i] <= a[m]);
  requires (forall i: int :: y <  i && i < n ==> a[i] <= a[m]);

  ensures bad || (0 <= x && x <= y && y < n);
  ensures bad || (m == x || m == y);
  ensures bad || (forall i: int :: 0 <= i && i < x ==> a[i] <= a[m]);
  ensures bad || (forall i: int :: y <  i && i < n ==> a[i] <= a[m]);
{
  if (!(x != y)) {
    bad := true;
  }
  if (a[x] <= a[y]) {
    x := x + 1;
    m := y;
  } else {
    y := y - 1;
    m := x;
  }

  if (!(x != y)) {
    bad := true;
  }
  if (a[x] <= a[y]) {
    x := x + 1;
    m := y;
  } else {
    y := y - 1;
    m := x;
  }
}

tff(a, type, a : $array($int, $int)).
tff(bad, type, bad : $o).
tff(m, type, m : $int).
tff(n, type, n : $int).
tff(x, type, x : $int).
tff(y, type, y : $int).
tff(voogie_precondition_1, axiom,
    $greater(n, 0)).
tff(voogie_precondition_2, axiom,
    (($lesseq(0, x) &
       $lesseq(x, y)) &
       $less(y, n))).
tff(voogie_precondition_3, axiom,
    ((m = x) |
       (m = y))).
tff(voogie_precondition_4, axiom,
    (! [I : $int] : ((($lesseq(0, I) &
                        $less(I, x)) =>
                        $lesseq($select(a, I), $select(a, m)))))).
tff(voogie_precondition_5, axiom,
    (! [I : $int] : ((($less(y, I) &
                        $less(I, n)) =>
                        $lesseq($select(a, I), $select(a, m)))))).
tff(voogie_conjecture, conjecture,
    $let(bad : $o,
         bad := $ite(~(x != y),
                     $true,
                     bad),
    $let([m : $int, y : $int, x : $int],
         [m, y, x] := $ite($lesseq($select(a, x), $select(a, y)),
                           $let(x : $int,
                                x := $sum(x, 1),
                           $let(m : $int,
                                m := y,
                                [m, y, x])),
                           $let(y : $int,
                                y := $difference(y, 1),
                           $let(m : $int,
                                m := x,
                                [m, y, x]))),
    $let(bad : $o,
         bad := $ite(~(x != y),
                     $true,
                     bad),
    $let([m : $int, y : $int, x : $int],
         [m, y, x] := $ite($lesseq($select(a, x), $select(a, y)),
                           $let(x : $int,
                                x := $sum(x, 1),
                           $let(m : $int,
                                m := y,
                                [m, y, x])),
                           $let(y : $int,
                                y := $difference(y, 1),
                           $let(m : $int,
                                m := x,
                                [m, y, x]))),
         ((bad |
            (($lesseq(0, x) &
               $lesseq(x, y)) &
               $less(y, n))) &
            ((bad |
               ((m = x) |
                  (m = y))) &
               ((bad |
                  (! [I : $int] : ((($lesseq(0, I) &
                                      $less(I, x)) =>
                                      $lesseq($select(a, I), $select(a, m)))))) &
                  (bad |
                     (! [I : $int] : ((($less(y, I) &
                                         $less(I, n)) =>
                                         $lesseq($select(a, I), $select(a, m)))))))))))))).