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!