# Counting the number of occurences - loop invariant

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?

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