method Find(a: array?<int>, key: int) returns (index: int)
   requires a != null;
   ensures index >= 0 ==> (index < a.Length && a[index] == key && (forall k :: 0 <= k < index ==> (a[k] != key)));
   ensures index < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != key;
{
   index := 0;
   while (index < a.Length)
   invariant 0 <= index <= a.Length;
   //invariant index < a.Length ==> a[index] != key;
   invariant forall k:int :: 0 <= k < index ==> a[k] != key;
   {
      if (a[index] == key) { return; }
      index := index + 1;
   }
   index := -1;
}