bool ceq(const char *s, const char *t, std::size_t n) {

int i=0, j=0, size=static_cast<int>(n), k;

while(i<n && j<size) {

for(k=0; k<size && s[(i+k)%size]==t[(j+k)%size]; ++k);

if(k==size) return true;

if(s[(i+k)%size]>t[(j+k)%size])

i+=k+1;

else

j+=k+1;

}

return false;

}

Given two strings and , this function returns true if and only if and are equivalent under circular shift. and are equivalent under circular shift if there is an index such that for any integer , .

It is easy to see that the worst case running time of this function is linear: The asymptotic running time is bounded by the total number of iterations executed by the inner “for” loop. In each iteration, the value of will be increased and ultimately, the increment will be accumulated into either variable or . When either or reaches , the function will return.

Why do I post this small piece of program? It is a perfect example to show a program can be short but still not easy to understand. It is also one of my favorite examples to convince people “loop invariant proof” is a good way to understand a program — if it is not the only way. You may load the program into your favorite debugger, and check closely how each single line is executed; you may feed it with all kind testing cases, and verify every output. But you simply cannot get enough insight to convince yourself why the program is correct. This is what I believe in: *Program should be proven to be correct; Testing should only be used to catch typos.*

How to prove this program is correct? Let us introduce several notations first.

**1.** Given string of length of , define .

**2.** Define . That is, the set of strings generated by shifting .

**3.** For a string and a set of strings , we call *beats * if there is a string such that .

4. For two set of strings and , we call *beats * if for any string , there exists a string such that .

**Claim**: and are equivalent if and only if neither beats nor beats . (Hints: If and are equivalent, then . So the minimum string in cannot beat vice versa.)

Our program holds such invariant: At the beginning of each iteration of the “while” loop, for any , beats ; for any , beats . We will skip the proof of the invariant since it is trivial. With this invariant, when the while loop stops we have either:

1. k==size: in this case, the two string are equivalent. (return true)

2. i>=size or j>=size: in this case, either beats or beats , so and are not equivalent by the claim. (return false)

P.S. The function returns false for empty strings () and one may argue that true should be returned instead.