#include "arrays.pi"

define int ix = ?;

@pre  0 <= l && u < length(a)
@post rv <-> exists(ix, l, u, a[ix] == e)
bool LinearSearch(int[] a, int l, int u, int e)
declare
  int i;
{
  for
    @ i >= l && forall(ix, l, i - 1, a[ix] != e)
    (i = l; i <= u; i = i + 1)
  {
    if (a[i] == e)
      return true;
  }
  return false;
}