Add more comments about Knuth-Morris-Pratt algorithm.

diff --git a/ChangeLog b/ChangeLog
index fc6647fba5b9a46d78c1ac840bbd2f23e586c77d..0578cf86c13db591775441a709be98be4b950eeb 100644 (file)
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,12 @@
+2007-12-23  Bruno Haible  <bruno@clisp.org>
+
+       * lib/c-strcasestr.c: Add more comments.
+       * lib/c-strstr.c: Likewise.
+       * lib/mbscasestr.c: Likewise.
+       * lib/mbsstr.c: Likewise.
+       * lib/strcasestr.c: Likewise.
+       * lib/memmem.c: Likewise.
+
 2007-12-23  Bruno Haible  <bruno@clisp.org>
 
        * tests/test-memmem.c: Include <string.h> first.

diff --git a/lib/c-strcasestr.c b/lib/c-strcasestr.c
index 2a075c060251fa678a419d31146b2b6baccc5599..76732d20ff74338543cf5072c40b4c7ca8687770 100644 (file)
--- a/lib/c-strcasestr.c
+++ b/lib/c-strcasestr.c
@@ -43,34 +43,67 @@ knuth_morris_pratt (const char *haystack, const char *needle,
   /* Fill the table.
      For 0 < i < m:
        0 < table[i] <= i is defined such that
-       rhaystack[0..i-1] == needle[0..i-1] and rhaystack[i] != needle[i]
-       implies
-       forall 0 <= x < table[i]: rhaystack[x..x+m-1] != needle[0..m-1],
+       forall 0 < x < table[i]: needle[x..i-1] != needle[0..i-1-x],
        and table[i] is as large as possible with this property.
+     This implies:
+     1) For 0 < i < m:
+          If table[i] < i,
+          needle[table[i]..i-1] = needle[0..i-1-table[i]].
+     2) For 0 < i < m:
+          rhaystack[0..i-1] == needle[0..i-1]
+          and exists h, i <= h < m: rhaystack[h] != needle[h]
+          implies
+          forall 0 <= x < table[i]: rhaystack[x..x+m-1] != needle[0..m-1].
      table[0] remains uninitialized.  */
   {
     size_t i, j;
 
+    /* i = 1: Nothing to verify for x = 0.  */
     table[1] = 1;
     j = 0;
+
     for (i = 2; i < m; i++)
       {
+       /* Here: j = i-1 - table[i-1].
+          The inequality needle[x..i-1] != needle[0..i-1-x] is known to hold
+          for x < table[i-1], by induction.
+          Furthermore, if j>0: needle[i-1-j..i-2] = needle[0..j-1].  */
        unsigned char b = c_tolower ((unsigned char) needle[i - 1]);
 
        for (;;)
          {
+           /* Invariants: The inequality needle[x..i-1] != needle[0..i-1-x]
+              is known to hold for x < i-1-j.
+              Furthermore, if j>0: needle[i-1-j..i-2] = needle[0..j-1].  */
            if (b == c_tolower ((unsigned char) needle[j]))
              {
+               /* Set table[i] := i-1-j.  */
                table[i] = i - ++j;
                break;
              }
+           /* The inequality needle[x..i-1] != needle[0..i-1-x] also holds
+              for x = i-1-j, because
+                needle[i-1] != needle[j] = needle[i-1-x].  */
            if (j == 0)
              {
+               /* The inequality holds for all possible x.  */
                table[i] = i;
                break;
              }
+           /* The inequality needle[x..i-1] != needle[0..i-1-x] also holds
+              for i-1-j < x < i-1-j+table[j], because for these x:
+                needle[x..i-2]
+                = needle[x-(i-1-j)..j-1]
+                != needle[0..j-1-(x-(i-1-j))]  (by definition of table[j])
+                   = needle[0..i-2-x],
+              hence needle[x..i-1] != needle[0..i-1-x].
+              Furthermore
+                needle[i-1-j+table[j]..i-2]
+                = needle[table[j]..j-1]
+                = needle[0..j-1-table[j]]  (by definition of table[j]).  */
            j = j - table[j];
          }
+       /* Here: j = i - table[i].  */
       }
   }
 

diff --git a/lib/c-strstr.c b/lib/c-strstr.c
index cc91b63d8910f306bd714268747fb3d1635f5b8f..58ae2c51cff6cf9625fc508cb544754674bd40ee 100644 (file)
--- a/lib/c-strstr.c
+++ b/lib/c-strstr.c
@@ -42,34 +42,67 @@ knuth_morris_pratt (const char *haystack, const char *needle,
   /* Fill the table.
      For 0 < i < m:
        0 < table[i] <= i is defined such that
-       rhaystack[0..i-1] == needle[0..i-1] and rhaystack[i] != needle[i]
-       implies
-       forall 0 <= x < table[i]: rhaystack[x..x+m-1] != needle[0..m-1],
+       forall 0 < x < table[i]: needle[x..i-1] != needle[0..i-1-x],
        and table[i] is as large as possible with this property.
+     This implies:
+     1) For 0 < i < m:
+          If table[i] < i,
+          needle[table[i]..i-1] = needle[0..i-1-table[i]].
+     2) For 0 < i < m:
+          rhaystack[0..i-1] == needle[0..i-1]
+          and exists h, i <= h < m: rhaystack[h] != needle[h]
+          implies
+          forall 0 <= x < table[i]: rhaystack[x..x+m-1] != needle[0..m-1].
      table[0] remains uninitialized.  */
   {
     size_t i, j;
 
+    /* i = 1: Nothing to verify for x = 0.  */
     table[1] = 1;
     j = 0;
+
     for (i = 2; i < m; i++)
       {
+       /* Here: j = i-1 - table[i-1].
+          The inequality needle[x..i-1] != needle[0..i-1-x] is known to hold
+          for x < table[i-1], by induction.
+          Furthermore, if j>0: needle[i-1-j..i-2] = needle[0..j-1].  */
        unsigned char b = (unsigned char) needle[i - 1];
 
        for (;;)
          {
+           /* Invariants: The inequality needle[x..i-1] != needle[0..i-1-x]
+              is known to hold for x < i-1-j.
+              Furthermore, if j>0: needle[i-1-j..i-2] = needle[0..j-1].  */
            if (b == (unsigned char) needle[j])
              {
+               /* Set table[i] := i-1-j.  */
                table[i] = i - ++j;
                break;
              }
+           /* The inequality needle[x..i-1] != needle[0..i-1-x] also holds
+              for x = i-1-j, because
+                needle[i-1] != needle[j] = needle[i-1-x].  */
            if (j == 0)
              {
+               /* The inequality holds for all possible x.  */
                table[i] = i;
                break;
              }
+           /* The inequality needle[x..i-1] != needle[0..i-1-x] also holds
+              for i-1-j < x < i-1-j+table[j], because for these x:
+                needle[x..i-2]
+                = needle[x-(i-1-j)..j-1]
+                != needle[0..j-1-(x-(i-1-j))]  (by definition of table[j])
+                   = needle[0..i-2-x],
+              hence needle[x..i-1] != needle[0..i-1-x].
+              Furthermore
+                needle[i-1-j+table[j]..i-2]
+                = needle[table[j]..j-1]
+                = needle[0..j-1-table[j]]  (by definition of table[j]).  */
            j = j - table[j];
          }
+       /* Here: j = i - table[i].  */
       }
   }
 

diff --git a/lib/mbscasestr.c b/lib/mbscasestr.c
index 592c815b90447a9f743b82099e062fd8fbbe68ed..a5491e4c9bfaed910185d5741af3816d9cc5969e 100644 (file)
--- a/lib/mbscasestr.c
+++ b/lib/mbscasestr.c
@@ -48,34 +48,67 @@ knuth_morris_pratt_unibyte (const char *haystack, const char *needle,
   /* Fill the table.
      For 0 < i < m:
        0 < table[i] <= i is defined such that
-       rhaystack[0..i-1] == needle[0..i-1] and rhaystack[i] != needle[i]
-       implies
-       forall 0 <= x < table[i]: rhaystack[x..x+m-1] != needle[0..m-1],
+       forall 0 < x < table[i]: needle[x..i-1] != needle[0..i-1-x],
        and table[i] is as large as possible with this property.
+     This implies:
+     1) For 0 < i < m:
+          If table[i] < i,
+          needle[table[i]..i-1] = needle[0..i-1-table[i]].
+     2) For 0 < i < m:
+          rhaystack[0..i-1] == needle[0..i-1]
+          and exists h, i <= h < m: rhaystack[h] != needle[h]
+          implies
+          forall 0 <= x < table[i]: rhaystack[x..x+m-1] != needle[0..m-1].
      table[0] remains uninitialized.  */
   {
     size_t i, j;
 
+    /* i = 1: Nothing to verify for x = 0.  */
     table[1] = 1;
     j = 0;
+
     for (i = 2; i < m; i++)
       {
+       /* Here: j = i-1 - table[i-1].
+          The inequality needle[x..i-1] != needle[0..i-1-x] is known to hold
+          for x < table[i-1], by induction.
+          Furthermore, if j>0: needle[i-1-j..i-2] = needle[0..j-1].  */
        unsigned char b = TOLOWER ((unsigned char) needle[i - 1]);
 
        for (;;)
          {
+           /* Invariants: The inequality needle[x..i-1] != needle[0..i-1-x]
+              is known to hold for x < i-1-j.
+              Furthermore, if j>0: needle[i-1-j..i-2] = needle[0..j-1].  */
            if (b == TOLOWER ((unsigned char) needle[j]))
              {
+               /* Set table[i] := i-1-j.  */
                table[i] = i - ++j;
                break;
              }
+           /* The inequality needle[x..i-1] != needle[0..i-1-x] also holds
+              for x = i-1-j, because
+                needle[i-1] != needle[j] = needle[i-1-x].  */
            if (j == 0)
              {
+               /* The inequality holds for all possible x.  */
                table[i] = i;
                break;
              }
+           /* The inequality needle[x..i-1] != needle[0..i-1-x] also holds
+              for i-1-j < x < i-1-j+table[j], because for these x:
+                needle[x..i-2]
+                = needle[x-(i-1-j)..j-1]
+                != needle[0..j-1-(x-(i-1-j))]  (by definition of table[j])
+                   = needle[0..i-2-x],
+              hence needle[x..i-1] != needle[0..i-1-x].
+              Furthermore
+                needle[i-1-j+table[j]..i-2]
+                = needle[table[j]..j-1]
+                = needle[0..j-1-table[j]]  (by definition of table[j]).  */
            j = j - table[j];
          }
+       /* Here: j = i - table[i].  */
       }
   }
 
@@ -154,34 +187,67 @@ knuth_morris_pratt_multibyte (const char *haystack, const char *needle,
   /* Fill the table.
      For 0 < i < m:
        0 < table[i] <= i is defined such that
-       rhaystack[0..i-1] == needle[0..i-1] and rhaystack[i] != needle[i]
-       implies
-       forall 0 <= x < table[i]: rhaystack[x..x+m-1] != needle[0..m-1],
+       forall 0 < x < table[i]: needle[x..i-1] != needle[0..i-1-x],
        and table[i] is as large as possible with this property.
+     This implies:
+     1) For 0 < i < m:
+          If table[i] < i,
+          needle[table[i]..i-1] = needle[0..i-1-table[i]].
+     2) For 0 < i < m:
+          rhaystack[0..i-1] == needle[0..i-1]
+          and exists h, i <= h < m: rhaystack[h] != needle[h]
+          implies
+          forall 0 <= x < table[i]: rhaystack[x..x+m-1] != needle[0..m-1].
      table[0] remains uninitialized.  */
   {
     size_t i, j;
 
+    /* i = 1: Nothing to verify for x = 0.  */
     table[1] = 1;
     j = 0;
+
     for (i = 2; i < m; i++)
       {
+       /* Here: j = i-1 - table[i-1].
+          The inequality needle[x..i-1] != needle[0..i-1-x] is known to hold
+          for x < table[i-1], by induction.
+          Furthermore, if j>0: needle[i-1-j..i-2] = needle[0..j-1].  */
        mbchar_t *b = &needle_mbchars[i - 1];
 
        for (;;)
          {
+           /* Invariants: The inequality needle[x..i-1] != needle[0..i-1-x]
+              is known to hold for x < i-1-j.
+              Furthermore, if j>0: needle[i-1-j..i-2] = needle[0..j-1].  */
            if (mb_equal (*b, needle_mbchars[j]))
              {
+               /* Set table[i] := i-1-j.  */
                table[i] = i - ++j;
                break;
              }
+           /* The inequality needle[x..i-1] != needle[0..i-1-x] also holds
+              for x = i-1-j, because
+                needle[i-1] != needle[j] = needle[i-1-x].  */
            if (j == 0)
              {
+               /* The inequality holds for all possible x.  */
                table[i] = i;
                break;
              }
+           /* The inequality needle[x..i-1] != needle[0..i-1-x] also holds
+              for i-1-j < x < i-1-j+table[j], because for these x:
+                needle[x..i-2]
+                = needle[x-(i-1-j)..j-1]
+                != needle[0..j-1-(x-(i-1-j))]  (by definition of table[j])
+                   = needle[0..i-2-x],
+              hence needle[x..i-1] != needle[0..i-1-x].
+              Furthermore
+                needle[i-1-j+table[j]..i-2]
+                = needle[table[j]..j-1]
+                = needle[0..j-1-table[j]]  (by definition of table[j]).  */
            j = j - table[j];
          }
+       /* Here: j = i - table[i].  */
       }
   }
 

diff --git a/lib/mbsstr.c b/lib/mbsstr.c
index 73145cbb851180d5723c8c2bddd545762e4ae716..f875207184ecb264ecb7a7145312347b8e9f4088 100644 (file)
--- a/lib/mbsstr.c
+++ b/lib/mbsstr.c
@@ -45,34 +45,67 @@ knuth_morris_pratt_unibyte (const char *haystack, const char *needle,
   /* Fill the table.
      For 0 < i < m:
        0 < table[i] <= i is defined such that
-       rhaystack[0..i-1] == needle[0..i-1] and rhaystack[i] != needle[i]
-       implies
-       forall 0 <= x < table[i]: rhaystack[x..x+m-1] != needle[0..m-1],
+       forall 0 < x < table[i]: needle[x..i-1] != needle[0..i-1-x],
        and table[i] is as large as possible with this property.
+     This implies:
+     1) For 0 < i < m:
+          If table[i] < i,
+          needle[table[i]..i-1] = needle[0..i-1-table[i]].
+     2) For 0 < i < m:
+          rhaystack[0..i-1] == needle[0..i-1]
+          and exists h, i <= h < m: rhaystack[h] != needle[h]
+          implies
+          forall 0 <= x < table[i]: rhaystack[x..x+m-1] != needle[0..m-1].
      table[0] remains uninitialized.  */
   {
     size_t i, j;
 
+    /* i = 1: Nothing to verify for x = 0.  */
     table[1] = 1;
     j = 0;
+
     for (i = 2; i < m; i++)
       {
+       /* Here: j = i-1 - table[i-1].
+          The inequality needle[x..i-1] != needle[0..i-1-x] is known to hold
+          for x < table[i-1], by induction.
+          Furthermore, if j>0: needle[i-1-j..i-2] = needle[0..j-1].  */
        unsigned char b = (unsigned char) needle[i - 1];
 
        for (;;)
          {
+           /* Invariants: The inequality needle[x..i-1] != needle[0..i-1-x]
+              is known to hold for x < i-1-j.
+              Furthermore, if j>0: needle[i-1-j..i-2] = needle[0..j-1].  */
            if (b == (unsigned char) needle[j])
              {
+               /* Set table[i] := i-1-j.  */
                table[i] = i - ++j;
                break;
              }
+           /* The inequality needle[x..i-1] != needle[0..i-1-x] also holds
+              for x = i-1-j, because
+                needle[i-1] != needle[j] = needle[i-1-x].  */
            if (j == 0)
              {
+               /* The inequality holds for all possible x.  */
                table[i] = i;
                break;
              }
+           /* The inequality needle[x..i-1] != needle[0..i-1-x] also holds
+              for i-1-j < x < i-1-j+table[j], because for these x:
+                needle[x..i-2]
+                = needle[x-(i-1-j)..j-1]
+                != needle[0..j-1-(x-(i-1-j))]  (by definition of table[j])
+                   = needle[0..i-2-x],
+              hence needle[x..i-1] != needle[0..i-1-x].
+              Furthermore
+                needle[i-1-j+table[j]..i-2]
+                = needle[table[j]..j-1]
+                = needle[0..j-1-table[j]]  (by definition of table[j]).  */
            j = j - table[j];
          }
+       /* Here: j = i - table[i].  */
       }
   }
 
@@ -146,34 +179,67 @@ knuth_morris_pratt_multibyte (const char *haystack, const char *needle,
   /* Fill the table.
      For 0 < i < m:
        0 < table[i] <= i is defined such that
-       rhaystack[0..i-1] == needle[0..i-1] and rhaystack[i] != needle[i]
-       implies
-       forall 0 <= x < table[i]: rhaystack[x..x+m-1] != needle[0..m-1],
+       forall 0 < x < table[i]: needle[x..i-1] != needle[0..i-1-x],
        and table[i] is as large as possible with this property.
+     This implies:
+     1) For 0 < i < m:
+          If table[i] < i,
+          needle[table[i]..i-1] = needle[0..i-1-table[i]].
+     2) For 0 < i < m:
+          rhaystack[0..i-1] == needle[0..i-1]
+          and exists h, i <= h < m: rhaystack[h] != needle[h]
+          implies
+          forall 0 <= x < table[i]: rhaystack[x..x+m-1] != needle[0..m-1].
      table[0] remains uninitialized.  */
   {
     size_t i, j;
 
+    /* i = 1: Nothing to verify for x = 0.  */
     table[1] = 1;
     j = 0;
+
     for (i = 2; i < m; i++)
       {
+       /* Here: j = i-1 - table[i-1].
+          The inequality needle[x..i-1] != needle[0..i-1-x] is known to hold
+          for x < table[i-1], by induction.
+          Furthermore, if j>0: needle[i-1-j..i-2] = needle[0..j-1].  */
        mbchar_t *b = &needle_mbchars[i - 1];
 
        for (;;)
          {
+           /* Invariants: The inequality needle[x..i-1] != needle[0..i-1-x]
+              is known to hold for x < i-1-j.
+              Furthermore, if j>0: needle[i-1-j..i-2] = needle[0..j-1].  */
            if (mb_equal (*b, needle_mbchars[j]))
              {
+               /* Set table[i] := i-1-j.  */
                table[i] = i - ++j;
                break;
              }
+           /* The inequality needle[x..i-1] != needle[0..i-1-x] also holds
+              for x = i-1-j, because
+                needle[i-1] != needle[j] = needle[i-1-x].  */
            if (j == 0)
              {
+               /* The inequality holds for all possible x.  */
                table[i] = i;
                break;
              }
+           /* The inequality needle[x..i-1] != needle[0..i-1-x] also holds
+              for i-1-j < x < i-1-j+table[j], because for these x:
+                needle[x..i-2]
+                = needle[x-(i-1-j)..j-1]
+                != needle[0..j-1-(x-(i-1-j))]  (by definition of table[j])
+                   = needle[0..i-2-x],
+              hence needle[x..i-1] != needle[0..i-1-x].
+              Furthermore
+                needle[i-1-j+table[j]..i-2]
+                = needle[table[j]..j-1]
+                = needle[0..j-1-table[j]]  (by definition of table[j]).  */
            j = j - table[j];
          }
+       /* Here: j = i - table[i].  */
       }
   }
 

diff --git a/lib/memmem.c b/lib/memmem.c
index 69d2edc2091e5cb9de5561ce570c23e8a79929c7..ae2c6ee932b1276200056c5e528a3ea6b6c83668 100644 (file)
--- a/lib/memmem.c
+++ b/lib/memmem.c
@@ -45,34 +45,67 @@ knuth_morris_pratt (const char *haystack, const char *last_haystack,
   /* Fill the table.
      For 0 < i < m:
        0 < table[i] <= i is defined such that
-       rhaystack[0..i-1] == needle[0..i-1] and rhaystack[i] != needle[i]
-       implies
-       forall 0 <= x < table[i]: rhaystack[x..x+m-1] != needle[0..m-1],
+       forall 0 < x < table[i]: needle[x..i-1] != needle[0..i-1-x],
        and table[i] is as large as possible with this property.
+     This implies:
+     1) For 0 < i < m:
+          If table[i] < i,
+          needle[table[i]..i-1] = needle[0..i-1-table[i]].
+     2) For 0 < i < m:
+          rhaystack[0..i-1] == needle[0..i-1]
+          and exists h, i <= h < m: rhaystack[h] != needle[h]
+          implies
+          forall 0 <= x < table[i]: rhaystack[x..x+m-1] != needle[0..m-1].
      table[0] remains uninitialized.  */
   {
     size_t i, j;
 
+    /* i = 1: Nothing to verify for x = 0.  */
     table[1] = 1;
     j = 0;
+
     for (i = 2; i < m; i++)
       {
+       /* Here: j = i-1 - table[i-1].
+          The inequality needle[x..i-1] != needle[0..i-1-x] is known to hold
+          for x < table[i-1], by induction.
+          Furthermore, if j>0: needle[i-1-j..i-2] = needle[0..j-1].  */
        unsigned char b = (unsigned char) needle[i - 1];
 
        for (;;)
          {
+           /* Invariants: The inequality needle[x..i-1] != needle[0..i-1-x]
+              is known to hold for x < i-1-j.
+              Furthermore, if j>0: needle[i-1-j..i-2] = needle[0..j-1].  */
            if (b == (unsigned char) needle[j])
              {
+               /* Set table[i] := i-1-j.  */
                table[i] = i - ++j;
                break;
              }
+           /* The inequality needle[x..i-1] != needle[0..i-1-x] also holds
+              for x = i-1-j, because
+                needle[i-1] != needle[j] = needle[i-1-x].  */
            if (j == 0)
              {
+               /* The inequality holds for all possible x.  */
                table[i] = i;
                break;
              }
+           /* The inequality needle[x..i-1] != needle[0..i-1-x] also holds
+              for i-1-j < x < i-1-j+table[j], because for these x:
+                needle[x..i-2]
+                = needle[x-(i-1-j)..j-1]
+                != needle[0..j-1-(x-(i-1-j))]  (by definition of table[j])
+                   = needle[0..i-2-x],
+              hence needle[x..i-1] != needle[0..i-1-x].
+              Furthermore
+                needle[i-1-j+table[j]..i-2]
+                = needle[table[j]..j-1]
+                = needle[0..j-1-table[j]]  (by definition of table[j]).  */
            j = j - table[j];
          }
+       /* Here: j = i - table[i].  */
       }
   }
 
@@ -164,7 +197,7 @@ memmem (const void *haystack, size_t haystack_len,
     size_t comparison_count = 0;
 
     /* Speed up the following searches of needle by caching its first
-       character.  */
+       byte.  */
     char b = *Needle++;
 
     for (;; Haystack++)
@@ -195,7 +228,7 @@ memmem (const void *haystack, size_t haystack_len,
         outer_loop_count++;
         comparison_count++;
         if (*Haystack == b)
-          /* The first character matches.  */
+          /* The first byte matches.  */
           {
             const char *rhaystack = Haystack + 1;
             const char *rneedle = Needle;

diff --git a/lib/strcasestr.c b/lib/strcasestr.c
index c5fb51f78c431ea3368e4aa4d8d48ed22335259f..27145dd37d5d442a694f17055c68253457b21c02 100644 (file)
--- a/lib/strcasestr.c
+++ b/lib/strcasestr.c
@@ -45,34 +45,67 @@ knuth_morris_pratt (const char *haystack, const char *needle,
   /* Fill the table.
      For 0 < i < m:
        0 < table[i] <= i is defined such that
-       rhaystack[0..i-1] == needle[0..i-1] and rhaystack[i] != needle[i]
-       implies
-       forall 0 <= x < table[i]: rhaystack[x..x+m-1] != needle[0..m-1],
+       forall 0 < x < table[i]: needle[x..i-1] != needle[0..i-1-x],
        and table[i] is as large as possible with this property.
+     This implies:
+     1) For 0 < i < m:
+          If table[i] < i,
+          needle[table[i]..i-1] = needle[0..i-1-table[i]].
+     2) For 0 < i < m:
+          rhaystack[0..i-1] == needle[0..i-1]
+          and exists h, i <= h < m: rhaystack[h] != needle[h]
+          implies
+          forall 0 <= x < table[i]: rhaystack[x..x+m-1] != needle[0..m-1].
      table[0] remains uninitialized.  */
   {
     size_t i, j;
 
+    /* i = 1: Nothing to verify for x = 0.  */
     table[1] = 1;
     j = 0;
+
     for (i = 2; i < m; i++)
       {
+       /* Here: j = i-1 - table[i-1].
+          The inequality needle[x..i-1] != needle[0..i-1-x] is known to hold
+          for x < table[i-1], by induction.
+          Furthermore, if j>0: needle[i-1-j..i-2] = needle[0..j-1].  */
        unsigned char b = TOLOWER ((unsigned char) needle[i - 1]);
 
        for (;;)
          {
+           /* Invariants: The inequality needle[x..i-1] != needle[0..i-1-x]
+              is known to hold for x < i-1-j.
+              Furthermore, if j>0: needle[i-1-j..i-2] = needle[0..j-1].  */
            if (b == TOLOWER ((unsigned char) needle[j]))
              {
+               /* Set table[i] := i-1-j.  */
                table[i] = i - ++j;
                break;
              }
+           /* The inequality needle[x..i-1] != needle[0..i-1-x] also holds
+              for x = i-1-j, because
+                needle[i-1] != needle[j] = needle[i-1-x].  */
            if (j == 0)
              {
+               /* The inequality holds for all possible x.  */
                table[i] = i;
                break;
              }
+           /* The inequality needle[x..i-1] != needle[0..i-1-x] also holds
+              for i-1-j < x < i-1-j+table[j], because for these x:
+                needle[x..i-2]
+                = needle[x-(i-1-j)..j-1]
+                != needle[0..j-1-(x-(i-1-j))]  (by definition of table[j])
+                   = needle[0..i-2-x],
+              hence needle[x..i-1] != needle[0..i-1-x].
+              Furthermore
+                needle[i-1-j+table[j]..i-2]
+                = needle[table[j]..j-1]
+                = needle[0..j-1-table[j]]  (by definition of table[j]).  */
            j = j - table[j];
          }
+       /* Here: j = i - table[i].  */
       }
   }