I'm trying to come up with loop invariant for the following program.

k = a[0]
m = 1
p = 1
while p < n:
    if a[p] == k:
        m += 1
    p += 1
return m

I belive this program returns the number equal to the number of occurences of element a[0] in my array "a".

I thought maybe this is a good cadidate:

|{i: 0 <= i <= n and a[0] == a[i]}| = m

Am I ok? If not, is this even the right direction to go?

  • 4
    $\begingroup$ $i\leq n$ should probably be $i<p$ instead, otherwise the invariant is false when the loop starts. $\endgroup$ – chi Feb 1 '18 at 23:51
  • $\begingroup$ Try proving it correct! $\endgroup$ – Raphael Feb 2 '18 at 7:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.