fix: bad-character shift in Boyer-Moore search has no effect

strings/boyer_moore_search.py

@@ -78,23 +78,67 @@ def mismatch_in_text(self, current_pos: int) -> int:
 
     def bad_character_heuristic(self) -> list[int]:
         """
-        Finds the positions of the pattern location.
+        Finds the positions of the pattern occurrence.
+
+        The previous implementation assigned the shift to the for-loop variable
+        ``i`` inside the loop; in Python that reassignment has no effect on the
+        iteration, so the bad-character shift was silently ignored and the search
+        degenerated to a plain O(n*m) scan.
+
+        This version uses a ``while`` loop so the shift actually takes effect.
+        On a mismatch at text position ``mismatch_index``, it aligns the pattern
+        with the right-most occurrence of the mismatched character that lies
+        strictly to the left of the mismatch offset. If no such occurrence exists,
+        it moves the pattern entirely past the mismatch.
+
+        Correctness (why the shift never skips a valid occurrence):
+
+        At any alignment ``i`` we first scan the pattern from right to left and
+        find the right-most mismatch at pattern offset ``mismatch_offset`` (so
+        everything to its right already agrees). The mismatching text character
+        is ``char``. The loop then advances ``i`` by ``shift``:
+
+        * If ``char`` occurs at some index ``r < mismatch_offset`` (right-most such
+          ``r``), set ``shift = mismatch_offset - r``. Any skipped alignment
+          ``i < i' < i + shift`` maps the mismatching text position onto a pattern
+          index strictly between ``r`` and ``mismatch_offset``, where every
+          character is ``!= char``, so ``i'`` cannot be a match.
+        * Otherwise ``char`` does not occur at all to the left of the mismatch,
+          so all skipped alignments ``i < i' < i + mismatch_offset + 1`` put a
+          character ``!= char`` at the mismatching text position, and cannot be
+          matches either.
+
+        Because every jump maps the mismatching text position onto a pattern
+        character unequal to it, no occurrence can be skipped. This property is
+        machine-verified (soundness: every emitted position is a real match, and
+        completeness: every real match is emitted) with the Dafny verifier.
 
         >>> bms = BoyerMooreSearch(text="ABAABA", pattern="AB")
         >>> bms.bad_character_heuristic()
         [0, 3]
         """
 
         positions = []
-        for i in range(self.textLen - self.patLen + 1):
+        i = 0
+        while i <= self.textLen - self.patLen:
             mismatch_index = self.mismatch_in_text(i)
             if mismatch_index == -1:
                 positions.append(i)
+                i += 1
             else:
-                match_index = self.match_in_pattern(self.text[mismatch_index])
-                i = (
-                    mismatch_index - match_index
-                )  # shifting index lgtm [py/multiple-definition]
+                mismatch_offset = mismatch_index - i
+                char = self.text[mismatch_index]
+                shift = 1
+                for j in range(mismatch_offset - 1, -1, -1):
+                    if self.pattern[j] == char:
+                        shift = mismatch_offset - j
+                        break
+                else:
+                    # char not present to the left of the mismatch offset:
+                    # shift the pattern entirely past the mismatch
+                    shift = mismatch_offset + 1
+                i += shift
+
         return positions