[mcguire]

Brute force string search:

    /*@
      // There is a partial match of the needle at location loc in the
      // haystack, of length len.
      predicate partial_match_at(char *needle, char *haystack, int loc, int len) =
        \forall int i; 0 <= i < len ==> needle[i] == haystack[loc + i];
     */

    /*@
      // There is a complete match of the needle at location loc in the
      // haystack.
      predicate match_at(char *needle, int n, char *haystack, int h, int loc) =
        \valid(needle + (0 .. n-1)) && 0 <= n < INT_MAX &&
        \valid(haystack + (0 .. h-1)) && 0 <= h < INT_MAX &&
        n <= h && loc <= h - n &&
        partial_match_at(needle, haystack, loc, n);
     */

    /*@
     requires \valid(needle + (0 .. n-1)) && 0 <= n < INT_MAX;
     requires \valid(haystack + (0 .. h-1)) && 0 <= h < INT_MAX;
     requires n <= h;
     assigns \nothing;
     ensures -1 <= \result <= (h-n);
     behavior success:
        ensures \result >= 0 ==> match_at(needle, n, haystack, h, \result);
     behavior failure:
        ensures \result == -1 ==>
          \forall int i; 0 <= i < h ==>
            !match_at(needle, n, haystack, h, i);
     */
    int
    brute_force (char *needle, int n, char *haystack, int h)
    {
      int i, j;
    
      /*@
        loop assigns i, j;
        loop invariant 0 <= i <= (h-n) + 1;
        loop invariant \forall int k; 0 <= k < i ==>
          !match_at(needle, n, haystack, h, k);
       */
      for (i = 0; i <= h - n; ++i) {
        /*@
          loop assigns j;
          loop invariant 0 <= j <= n;
          loop invariant partial_match_at(needle, haystack, i, j);
        */
        for (j = 0; j < n && needle[j] == haystack[j + i]; ++j);
        if (j >= n) {
          return i;
        }
      }
      return -1;
    }