What I've Learned About Formal Methods in Half a Year(jakob.space)

  lemma nat.add_comm : ∀ n m : ℕ, n + m = m + n
  | n 0     := eq.symm (nat.zero_add n)
  | n (m+1) :=
    suffices succ (n + m) = succ (m + n), from
      eq.symm (succ_add m n) ▸ this,
    congr_arg succ (add_comm n m)

  lemma add_comm (a b : ℕ) : a + b = b + a :=
  begin
    induction a with a IH,
    rw (add_zero b),
    rw (zero_add b),
    trivial,
    rw (add_succ b a),
    rw (succ_add a b),
    rw IH,
    trivial
  end

    /*@
      // 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;
    }