caps_lock

Untitled

Mar 31st, 2015
289
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. method strf(a:array<char>, n:int, b:array<char>, m:int) returns (pos:int)
  2. requires a!=null && a.Length > n >= 0;
  3. requires b!=null && b.Length > m >= 0;
  4. requires n>=m;
  5. ensures -1 <= pos <= n-m;
  6. ensures pos >= 0 ==> forall k::0<=k<m ==> b[k]==a[pos+k];
  7. {
  8.   pos := -1;
  9.   var i:int := 0;
  10.   while (i<n-m+1)
  11.   invariant 0<=i<=n;
  12.   {
  13.     var j:int := i;
  14.     while (j<m)
  15.     invariant 0<=j<=m;
  16.     invariant forall k:: 0<=k<j ==> b[k] == a[i+k];
  17.     {
  18.      if (a[i+j] != b[j]) { break; }
  19.      j := j + 1;        
  20.     }
  21.     if (i==m){
  22.       assert forall k:: 0<=k<m ==> b[k] == a[i+k];
  23.       return i;
  24.     }
  25.     i := i + 1;
  26.   }
  27. }
  28.  
  29. TODO - write post stronger postcondition to this stuff.
RAW Paste Data