An array find method verification from http://rjoshi.org/cs116/homework/hw1-find.dfy

dafny-find

method find(A:array<int>, key: int) returns (k:int)
  requires A != null && A.Length > 0 ;
	requires A[0] < A[A.Length-1] ;
	ensures 0 <= k < A.Length-1 ;
	ensures A[k] < A[k+1] ;
{
	var i:int := 0;
  while(i < A.length) {
    if(A[i] == key) {
      return i;
    }
    i := i+1;
  }
  return i;
}