0
$\begingroup$

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?

Improve this question
$\endgroup$
2
  • 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

0

Reset to default

Your Answer

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