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, 2018 at 23:51
  • $\begingroup$ Try proving it correct! $\endgroup$
    – Raphael
    Feb 2, 2018 at 7:51


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.