method strf(a:array<char>, n:int, b:array<char>, m:int) returns (pos:int)
requires a!=null && a.Length > n >= 0;
requires b!=null && b.Length > m >= 0;
requires n>=m;
ensures -1 <= pos <= n-m;
ensures pos >= 0 ==> forall k::0<=k<m ==> b[k]==a[pos+k];
{
  pos := -1;
  var i:int := 0;
  while (i<n-m+1)
  invariant 0<=i<=n;
  {
    var j:int := i;
    while (j<m)
    invariant 0<=j<=m;
    invariant forall k:: 0<=k<j ==> b[k] == a[i+k];
    {
     if (a[i+j] != b[j]) { break; }
     j := j + 1;
    }
    if (i==m){
      assert forall k:: 0<=k<m ==> b[k] == a[i+k];
      return i;
    }
    i := i + 1;
  }
}

TODO - write post stronger postcondition to this stuff.