int LinearSearch(int [] a, int l, int r, int e) {
  int i;
  @pre ls {0 <= l && l <= r && r < scasize(a); }

  i = l;
  while ( i <=  r ) {
      if ( a[i] == e) {
          i = r;
      }  else {
          i = i + 1;
      }
  }
  return -1;

  @post ls {
    (0 <= l && l <= r && r < scasize(a) );
    ( (rv != -1) -> (l <= rv && rv <= r && a[rv] == e));
    ( (rv == -1) -> (forall(int k:[0 .. scasize(a) - 1]) {e != a[k]} ) );
  }

  @behavior ls {
    good { input={a={1,2,3},       l=0, r=2, e=4};        output={rv=-1}};
    good { input={a={1,2,3,4,5},   l=0, r=4, e=2};    output={rv=1}};
    bad  { input={a={1,2,3},       l=0, r=2, e=4};        output={rv=0}};
    bad  { input={a={5,2,7,6,3,8}, l=1, r=4, e=7};  output={rv=-1}};
    good { input={a={5,2,7,6,3,8}, l=4, r=1, e=7};  output={rv=-1}};
    good { input={a={5,2,7,6,3,8}, l=0, r=1, e=7};  output={rv=-1}};
    good { input={a={5,2,7,6,3,8}, l=-1, r=1, e=7}; output={rv=-1}};
  } 
}