# Help Finding Loop Invariant From For Loop

I have created the algorithm below...

        String A = v;
int val = 1;

for (int i = 1; i < v.length; i++) {
if (val == 0) {
A = v[i];
val++;
} else if (v[i].equals(A))
val++;
else
val--;
}


The goal of the algorithm is to find the item that occurs in more than half the array.

Let v = {"one", "two", "one", "three", "one", "two", "two", "one", "one"}

The string "one" occurs 5 out of 9 times. So, at the end of the loop, the String A will be equal to "one".

I'm lost as to how to derive a loop invariant from this. Could someone provide me with some direction?

• What is the goal of this loop, in words? – Dave Clarke Sep 13 '12 at 19:15
• I can't see how the algorithm does what you claim it does. – Dave Clarke Sep 13 '12 at 19:49
• what if no such string exists as in {"one","two","three"} – miracle173 Sep 14 '12 at 6:18
• @miracle173 I think that in that case, the result is undefined. In other words, it's allowed to be anything. – svick Sep 14 '12 at 9:06
• yes, if nothing occurs more than half the time, it is undefined. – MCR Sep 14 '12 at 15:43

The invariant at step $i$ is:
• A occurs at least in val cells of v[0..i]
• The remaining (i + 1 - val) cells can be discarded without changing the majority element.