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

[bolverk]

Fix bad-character shift having no effect (dead loop variable)

Fixes #14844

Summary

bad_character_heuristic() in strings/boyer_moore_search.py assigned the
computed shift to the for-loop variable i:

for i in range(self.textLen - self.patLen + 1):
    ...
    i = (mismatch_index - match_index)  # no effect: next iteration overwrites i

In Python, reassigning a for-loop variable inside the loop body has no effect
on the iteration sequence, so the shift was dead code and the search silently ran
as a plain O(n·m) scan over every position.

The rewrite uses a while loop so the shift actually advances the search, and
computes the shift in the pattern's coordinate space (the mismatch offset and
the alignment target are both pattern indices), instead of mixing a text index
with a pattern index as the old code did.

Correctness

The new algorithm was first written in Dafny and machine-verified (15 proof
obligations, 0 errors machine-checked by the SMT-based verifier) to establish:

• Soundness — every emitted position is a genuine occurrence of pattern.
• Completeness — no occurrence is skipped by the shift.

The key safety invariant is documented in the docstring: a jump maps the
mismatching text position onto a pattern index that carries a character unequal
to it, so no skipped alignment can be a match.

In addition to the proof, the implementation agrees with a brute-force scan on
30,000 randomized inputs (empty text, single-character and repeated patterns).

Impact (the issue's own reproduction)

text = "ABCDEFGHIJKLMNOPABCDEFGHIJKLMNOP", pattern = "MNOP":

	iterations	matches
before (brute-force)	29	[12, 28]
after	9	[12, 28]

The existing doctest BoyerMooreSearch("ABAABA", "AB").bad_character_heuristic()
still returns [0, 3].

Checklist

• Fix a bug or typo in an existing algorithm
• I have read CONTRIBUTING.md
• This pull request is all my own work
• This PR only changes one algorithm file
• Passes ruff check, ruff format --check, and the doctests

[daltino]

The fix itself is correct — reassigning a for-loop variable in Python is indeed a no-op and the while-loop rewrite is the right approach. That said, the diff is a bit hard to evaluate in isolation because it doesn't show the full updated implementation; I'd want to verify the shift calculation specifically: the bad-character shift should be max(1, mismatch_offset - last_occurrence) where last_occurrence is the rightmost index of the mismatched character in the pattern to the left of mismatch_offset — making sure it's clamped to at least 1 is critical to avoid an infinite loop when the character appears at or to the right of the mismatch position. It would also strengthen the PR significantly to add a test case that would have caught the original bug — something like asserting that a pattern search on a long string of repeated characters completes in sub-quadratic time or simply verifying correct positions are returned for a case where the bad-character shift should skip multiple positions at once.

[bolverk]

I added a test to verify the issue does not recur. Since it's a performance issue I resorted to a monkey patch to count the number of iterations.
I also changed the while loop to a for loop with the maximum possible number of iterations. If the number of iterations exceeds then we fall back to brute force, but this should never happen.

[priya-sundaram-dev]

Approving. This is a real bug and a solid fix.

The root cause is exactly as described: for i in range(...) followed by i = mismatch_index - match_index inside the body — in Python that reassignment is overwritten by the next iteration, so the bad-character shift was dead code and the search silently degraded to an O(n·m) brute scan. Switching to an explicit index advanced by a while/accumulator loop is the right shape.

Computing the shift in the pattern's coordinate space (mismatch_offset = mismatch_index - i, then scanning pattern[mismatch_offset-1 .. 0] for the mismatched char, else jumping mismatch_offset + 1) is the correct classic bad-character rule and, crucially, it always advances by ≥1, so termination is guaranteed.

I verified correctness against a brute-force oracle:

• Exhaustive, binary alphabet, all patterns/texts up to len 4/9: 30,380 cases, 0 mismatches.
• Randomized over 3–4 char alphabets, lengths up to 14: 300,000 cases, 0 mismatches.
• The 13 doctests pass, and the added call-counting doctest confirms the shift actually fires (9 mismatch_in_text calls vs 29 for brute force on the sample), which is the exact behaviour the old code failed to deliver.

One small, non-blocking note: the for/else brute-force safety net is effectively unreachable now that every branch advances i by at least 1 (the if i > textLen - patLen: break guard always trips first). It's harmless defensive code — fine to keep, just worth a comment that it's a belt-and-suspenders fallback rather than a reachable path.

LGTM. 👍