# Trouble finding loop invariant for this while loop

I'm having trouble coming up with an invariant for proving partial correctness of this function.

def f(A):
# Pre: A is a list of integers
# Post: Returns true if and only if there is an even number of positive
# numbers in A

even = True
i = 0
while i < A.length:
if A[i] > 0:
even = not even
i = i + 1
return even


So far, I have something like:

i <= A.length and (even == True or even == False)


However, I don't really know whether this is correct or, if it is even, if I can prove that it is inductive. I don't really know how to start the proof and was just looking for some help to point me in the right direction.

Thanks.

• You could try something like this: even == True if and only if the number of positive numbers in A[0..i-1] is even – Anton Trunov Nov 20 '15 at 20:20

Unfortunately, you can't prove partial correctness of your algorithm because it is incorrect.

EDIT: The algorithm provided is indeed correct.

Aditionally, you can't prove that an algorithm is "inductive". You can prove its correctness by using loop invariants,which are quite similar to mathematical inductions.

We must show three things about a loop invariant:

# Initialization:

Before you start the loop,check if your initialization is correct.

You want to check if there is an even number of positive numbers in your list A. You set up the variable i to equal 0, therefore your loop begins at the first index of your list.

The variable even is set to True. If it were set to false, and you had 0 positive integers, it would return false, which is incorrect. Therefore, initialization is correct.

You can see initialization as your base case.

# Maintenance:

If your invariant holds from iteration to iteration.

The body of your while loop checks if an integer in index i of your array A is positive. If that condition is true, it sets the boolean variable "even" to "not even".

Since it flips the value of even equal to the amount of positive integers in your list,the maintenance is correct.

# Termination:

What happens when the loop is over?

The last step increments the variable i by 1. When the loop ends, i < A.length, which is correct.

The algorithm will return either True or False based on the amount of positive integers. Since initialization and maintenance are correct, the algorithm is correct.

• The algorithm is correct. even starts off as True. Then, as the loop runs, whenever a number is positive, it flips the boolean value of even. If there are an even number of positive numbers, even = not even will execute an even which means it will end up as true. If there is an odd number of positive numbers, even = not even will execute an odd number of times which means it will end up as false. Therefore, the algorithm will return true if and only if there are an even number of positive numbers in A. – AWPgod Nov 20 '15 at 18:57
• You're right, the algorithm you provided is correct. – eegodinez Nov 20 '15 at 19:07

Let's rewrite your code so that everything is explicit.

{ 0 ≤ n }
e ≔ true; i ≔ 0;
while i < n:
if a[i] > 0 then e ≔ ¬ e;
i  ≔ i + 1;
{ e ≈ even (# j : 0..n-1 • a[j] > 0) }


where we have used n in place of a.length and the notation (# x • p) returns the number of items x that satisfy p: formally

(# x : a..b • px) = 0                                             ; if a > b
(# x : a..b • px) = (IF p(b) THEN 1 ELSE 0) + (# x : a..b-1 • px) ; if a ≤ b


Now after the loop is finished we will know that necessarily n ≤ i and that together with whatever the invariant is, call it P, we can establish the post-condition:

  n ≤ i ∧ P ⇒ e ≈ even (# j : 0..n-1 • a[j] > 0)
⇐⟨ arithmetic ; assuming i ≤ n ⟩
n ≤ i ≤ n ∧ P ⇒ e ≈ even (# j : 0..i-1 • a[j] > 0)
⇐⟨ one possible solution ⟩
P ≡ (i ≤ n ∧ e ≈ even (# j : 0..i-1 • a[j] > 0) )


Notice that we "calculated" P from what we know about the post-condition and the loop-guard! Moreover, the formulation found above leads to a nifty intuitive interpretation:

e if true precisely when we've encountered an even number of positive integers so far


Anyhow, we've chosen as invariant

P : i ≤ n ∧ e ≈ even (# j : 0..i-1 • a[j] > 0)


For it to be an invaraint, it must be initaly true before the loop begins:

  { 0 ≤ n } e ≔ true; i ≔ 0 { P }
≡⟨ assignment rule, twice ⟩
0 ≤ n ⇒ P [ i / 0] [true / e]
≡⟨ definitions ⟩
0 ≤ n ⇒ 0 ≤ n ∧ e ≈ even (# j : 0..0-1 • a[j] > 0)
≡⟨ there are no i with 0 ≤ i ≤ -1 so the count is 0 ⟩
0 ≤ n ⇒ 0 ≤ n ∧ e ≈ even 0
≡⟨ arithmetic ; 0 is even ⟩
true


Also it must be maintained by the loop body,

 {P ∧ i < n} if a[i] > 0 then e ≔ ¬ e; i  ≔ i + 1; {P}
≡⟨ assignment rule ⟩
{P ∧ i < n} if a[i] > 0 then e ≔ ¬ e {P [i+1 / i] }


Now there are two cases to consider depending on wheather a[i] > 0 holds or not.

Easy case. assume it does not hold, a[i] ≤ 0, then we must prove P [i+1 / i] assuming P ∧ i < n:

   P [i+1 / i]
≡⟨ definition ⟩
i+1 ≤ n ∧ e ≈ even (# j : 0..i+1-1 • a[j] > 0)
≡⟨ assumption i < n yields i+1 ≤ n ⟩
e ≈ even (# j : 0..i+1-1 • a[j] > 0)
≡⟨ definition of count quantifier ⟩
e ≈ even ( (IF a[i] > 0 THEN 1 ELSE 0) + (# j : 0..i-1 • a[j] > 0))
≡⟨ arithmetic: even (m + n) ≡ even m ≡ even n ⟩
e ≈ ( even (IF a[i] > 0 THEN 1 ELSE 0) ≡ even (# j : 0..i-1 • a[j] > 0) )
≡⟨ assumption P yields e ≈ even (# j : 0..i-1 • a[j] > 0) ⟩
e ≈ ( even (IF a[i] > 0 THEN 1 ELSE 0) ≡ e )
≡⟨ case assumption a[i] ≤ 0 ⟩
e ≈ ( even 0 ≡ e )
≡⟨ 0 is an even number and (true ≡ p) ≈ p ⟩
e ≈ e
≡⟨ reflexitivity ⟩
true


Sweet! One more case to go!

Hard case assume it does hold, a[i] > 0, then we must prove P [i+1 / i] [¬ e / e] assuming P ∧ i < n:

   P [i+1 / i] [¬ e / e]
≡⟨ definitions ⟩
i+1 ≤ n ∧ ¬ e ≈ even (# j : 0..i+1-1 • a[j] > 0)
≡⟨ assumption i < n yields i+1 ≤ n ⟩
¬ e ≈ even (# j : 0..i+1-1 • a[j] > 0)
≡⟨ definition of count quantifier ⟩
¬ e ≈ even ( (IF a[i] > 0 THEN 1 ELSE 0) + (# j : 0..i-1 • a[j] > 0) )
≡⟨ case assumption a[i] > 0 ⟩
¬ e ≈ even (1 + (# j : 0..i-1 • a[j] > 0) )
≡⟨ arithmetic: even (m + n) ≡ even m ≡ even n ⟩
¬ e ≈ (even 1 ≡ even (# j : 0..i-1 • a[j] > 0))
≡⟨ assumption P yields e ≈ even (# j : 0..i-1 • a[j] > 0) ⟩
¬ e ≈ (even 1 ≡ e)
≡⟨ 1 is not even and (false ≡ p) ≈ ¬ p ⟩
¬ e ≈ ¬ e
≡⟨ reflexitivity ⟩
true


Sweet! However, we've only proven "partial correctness". To show total correctness we need to prove that the loop termiantes. That is we need a bound function bf that is intially positive and is decreased by the loop-body. Since the loop guard is i < n we may choose

     bf : n - i


and the loop guard ensures that it is initally positive:

  i < n ⇒ 0 < n - i ⇒ 0 < bf


It remains to show that the loop-body decreases it: for any t, we must show

   { bf = t } if a[i] > 0 then e ≔ ¬ e; i  ≔ i + 1; { bf < t }
≡⟨ assignment rule ; definitions ⟩
{ n - i = t } if a[i] > 0 then e ≔ ¬ e; i  ≔ i + 1; { n - (i + 1) < t }
≡⟨ conditional rule; but post-condition makes no use of e so can be ignored ⟩
n - i = t ⇒ n - i -1 < t
≡⟨ arithmetic ⟩
true


Sweet; that was fun!

Best of luck!