SE 504
Sample Proof of Correctness of an If-Else Command

Prove the following Hoare triple: 

{k ≠ 1}
if k ≥ -1 then k := k-1
else k := k+1
fi
{k ≠ 0}

The Hoare Triple If-Else Law (HTIEL) says 

{P} if B then S else T fi {Q}  ≡  {P ∧ B} S {Q} ∧ {P ∧ ¬B} T {Q}

Thus, to prove the given Hoare Triple, it suffices to prove each of the following Hoare Triples:

  1. {k≠1 ∧ k≥-1} k:=k-1 {k≠0}
  2. {k≠1 ∧ ¬(k≥-1)} k:=k+1 {k≠0}

In each of these, the program is simply an assignment command; hence we use the Hoare Triple Assignment Law, which says {P} x := E {Q} ≡ [P ⇒ Q(x:=E)], to prove each one. In both cases, we prove the relevant implication using the Assume the Antecedant approach. 

Assume k≠1 and k≥-1.

    (k≠0)(k:=k-1)

=      < textual substitution >

    k-1 ≠ 0

=      < algebra >

    k ≠ 1 

=      < assumption k≠1 >

    true
 
Assume k≠1 and ¬(k≥-1)

    (k≠0)(k:=k+1)

=      < textual substitution >

    k+1 ≠ 0

=      < algebra >

    k ≠ -1 

=      < assumption ¬(k≥-1), 
         which is equivalent to k<-1 >

    true