Trouble finding loop invariant for this while loop

Question

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.

Answer 1

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.

Answer 2

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!