[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
comments about Knuth-Morris-Pratt algorithm
|
From: |
Bruno Haible |
|
Subject: |
comments about Knuth-Morris-Pratt algorithm |
|
Date: |
Wed, 26 Dec 2007 16:10:23 +0100 |
|
User-agent: |
KMail/1.9.1 |
Hi,
Some of the comments in the KMP algorithm implementation were insufficient
to understand and verify the correctness of the code. I'm adding better
comments.
2007-12-23 Bruno Haible <address@hidden>
* 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.
*** lib/c-strcasestr.c.orig 2007-12-23 21:06:01.000000000 +0100
--- lib/c-strcasestr.c 2007-12-23 21:02:06.000000000 +0100
***************
*** 43,76 ****
/* 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],
and table[i] is as large as possible with this property.
table[0] remains uninitialized. */
{
size_t i, j;
table[1] = 1;
j = 0;
for (i = 2; i < m; i++)
{
unsigned char b = c_tolower ((unsigned char) needle[i - 1]);
for (;;)
{
if (b == c_tolower ((unsigned char) needle[j]))
{
table[i] = i - ++j;
break;
}
if (j == 0)
{
table[i] = i;
break;
}
j = j - table[j];
}
}
}
--- 43,109 ----
/* Fill the table.
For 0 < i < m:
0 < table[i] <= i is defined such that
! 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]. */
}
}
*** lib/c-strstr.c.orig 2007-12-23 21:06:01.000000000 +0100
--- lib/c-strstr.c 2007-12-23 20:57:17.000000000 +0100
***************
*** 42,75 ****
/* 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],
and table[i] is as large as possible with this property.
table[0] remains uninitialized. */
{
size_t i, j;
table[1] = 1;
j = 0;
for (i = 2; i < m; i++)
{
unsigned char b = (unsigned char) needle[i - 1];
for (;;)
{
if (b == (unsigned char) needle[j])
{
table[i] = i - ++j;
break;
}
if (j == 0)
{
table[i] = i;
break;
}
j = j - table[j];
}
}
}
--- 42,108 ----
/* Fill the table.
For 0 < i < m:
0 < table[i] <= i is defined such that
! 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]. */
}
}
*** lib/mbscasestr.c.orig 2007-12-23 21:06:01.000000000 +0100
--- lib/mbscasestr.c 2007-12-23 21:02:08.000000000 +0100
***************
*** 48,81 ****
/* 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],
and table[i] is as large as possible with this property.
table[0] remains uninitialized. */
{
size_t i, j;
table[1] = 1;
j = 0;
for (i = 2; i < m; i++)
{
unsigned char b = TOLOWER ((unsigned char) needle[i - 1]);
for (;;)
{
if (b == TOLOWER ((unsigned char) needle[j]))
{
table[i] = i - ++j;
break;
}
if (j == 0)
{
table[i] = i;
break;
}
j = j - table[j];
}
}
}
--- 48,114 ----
/* Fill the table.
For 0 < i < m:
0 < table[i] <= i is defined such that
! 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,187 ****
/* 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],
and table[i] is as large as possible with this property.
table[0] remains uninitialized. */
{
size_t i, j;
table[1] = 1;
j = 0;
for (i = 2; i < m; i++)
{
mbchar_t *b = &needle_mbchars[i - 1];
for (;;)
{
if (mb_equal (*b, needle_mbchars[j]))
{
table[i] = i - ++j;
break;
}
if (j == 0)
{
table[i] = i;
break;
}
j = j - table[j];
}
}
}
--- 187,253 ----
/* Fill the table.
For 0 < i < m:
0 < table[i] <= i is defined such that
! 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]. */
}
}
*** lib/mbsstr.c.orig 2007-12-23 21:06:01.000000000 +0100
--- lib/mbsstr.c 2007-12-23 21:04:12.000000000 +0100
***************
*** 45,78 ****
/* 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],
and table[i] is as large as possible with this property.
table[0] remains uninitialized. */
{
size_t i, j;
table[1] = 1;
j = 0;
for (i = 2; i < m; i++)
{
unsigned char b = (unsigned char) needle[i - 1];
for (;;)
{
if (b == (unsigned char) needle[j])
{
table[i] = i - ++j;
break;
}
if (j == 0)
{
table[i] = i;
break;
}
j = j - table[j];
}
}
}
--- 45,111 ----
/* Fill the table.
For 0 < i < m:
0 < table[i] <= i is defined such that
! 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,179 ****
/* 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],
and table[i] is as large as possible with this property.
table[0] remains uninitialized. */
{
size_t i, j;
table[1] = 1;
j = 0;
for (i = 2; i < m; i++)
{
mbchar_t *b = &needle_mbchars[i - 1];
for (;;)
{
if (mb_equal (*b, needle_mbchars[j]))
{
table[i] = i - ++j;
break;
}
if (j == 0)
{
table[i] = i;
break;
}
j = j - table[j];
}
}
}
--- 179,245 ----
/* Fill the table.
For 0 < i < m:
0 < table[i] <= i is defined such that
! 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]. */
}
}
*** lib/memmem.c.orig 2007-12-23 21:06:01.000000000 +0100
--- lib/memmem.c 2007-12-23 20:59:19.000000000 +0100
***************
*** 45,78 ****
/* 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],
and table[i] is as large as possible with this property.
table[0] remains uninitialized. */
{
size_t i, j;
table[1] = 1;
j = 0;
for (i = 2; i < m; i++)
{
unsigned char b = (unsigned char) needle[i - 1];
for (;;)
{
if (b == (unsigned char) needle[j])
{
table[i] = i - ++j;
break;
}
if (j == 0)
{
table[i] = i;
break;
}
j = j - table[j];
}
}
}
--- 45,111 ----
/* Fill the table.
For 0 < i < m:
0 < table[i] <= i is defined such that
! 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,170 ****
size_t comparison_count = 0;
/* Speed up the following searches of needle by caching its first
! character. */
char b = *Needle++;
for (;; Haystack++)
--- 197,203 ----
size_t comparison_count = 0;
/* Speed up the following searches of needle by caching its first
! byte. */
char b = *Needle++;
for (;; Haystack++)
***************
*** 195,201 ****
outer_loop_count++;
comparison_count++;
if (*Haystack == b)
! /* The first character matches. */
{
const char *rhaystack = Haystack + 1;
const char *rneedle = Needle;
--- 228,234 ----
outer_loop_count++;
comparison_count++;
if (*Haystack == b)
! /* The first byte matches. */
{
const char *rhaystack = Haystack + 1;
const char *rneedle = Needle;
*** lib/strcasestr.c.orig 2007-12-23 21:06:01.000000000 +0100
--- lib/strcasestr.c 2007-12-23 21:05:40.000000000 +0100
***************
*** 45,78 ****
/* 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],
and table[i] is as large as possible with this property.
table[0] remains uninitialized. */
{
size_t i, j;
table[1] = 1;
j = 0;
for (i = 2; i < m; i++)
{
unsigned char b = TOLOWER ((unsigned char) needle[i - 1]);
for (;;)
{
if (b == TOLOWER ((unsigned char) needle[j]))
{
table[i] = i - ++j;
break;
}
if (j == 0)
{
table[i] = i;
break;
}
j = j - table[j];
}
}
}
--- 45,111 ----
/* Fill the table.
For 0 < i < m:
0 < table[i] <= i is defined such that
! 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]. */
}
}
| [Prev in Thread] |
Current Thread |
[Next in Thread] |
- comments about Knuth-Morris-Pratt algorithm,
Bruno Haible <=