// Given non-empty array `a`, this program returns an index of `a` 
// pointing to a minimum element of `a`. 
// Supposedly valid.
minind(a:[]int | r:int) { 
   assume #a > 0 ;
   var min:int, i:int {
       i   := 0;
       min := a[i]; 
       r   := i;
       while i < #a do { 
          if a[i] < min then {
             min := a[i];
             r   := i
          } 
          else { skip };
          i := i + 1
      }
   } ;
   assert (0<= r) && (r < #a) &&
          (forall i :: ((0<=i && (i< #a)) ==>  (a[i] >= a[r]))) 
}