/*@ predicate isMin(integer n, int *x, int m) =
  @   (\forall integer i; 0 <= i < n ==> x[i] >= m) &&
  @   (\exists integer i; 0 <= i < n && x[i] == m);
  @*/

/*@ requires  n > 0;
  @ requires  \valid(x + (0 .. n-1));
  @ assigns   \nothing;
  @ ensures   isMin(n, x, \result);
  @*/
int findmin(int n, int x[]) {
  int m = x[0];
  /*@ loop invariant  1 <= i <= n;
    @ loop invariant  isMin(i, x, m);
    @ loop assigns    i, m;
    @ loop variant    n-i;
    @*/
  for (int i = 1; i < n; ++i) if (x[i] < m) m = x[i];
  return m;
}