Proving Hoare's assignment axiom from Floyd's:

  1. {P[E/V]} V := E {EXISTS v. V = E[v/V] /\ (P[E/V])[v/V]}   by Floyd's axiom
  2. (EXISTS v. V = E[v/V] /\ (P[E/V])[v/V]) ==> P             by logic below
  3. {P[E/V]} V := E {P}                                       by postcondition weakening 1. and 2.

Lemma:

      (EXISTS v. V = E[v/V] /\ (P[E/V])[v/V])
    = (EXISTS v. V = E[v/V] /\ (P[E[v/V]/V]))
    = (EXISTS v. V = E[v/V] /\ (P[V/V]))
    = (EXISTS v. V = E[v/V] /\ P)
    = (EXISTS v. V = E[v/V]) /\ P
  ==> P


Proving Floyd's assignment axiom from Hoare's:

  1. {(EXISTS v. V = E[v/V] /\ P[v/V])[E/V]} V := E
     {(EXISTS v. V = E[v/V] /\ P[v/V])}                        by Hoare's axiom
  2. P ==> (EXISTS v. V = E[v/V] /\ P[v/V])[E/V]               by logic below
  3. {P} V := E {EXISTS v. V = E[v/V] /\ P[v/V]}               by precondition strengthening

Lemma:

     (EXISTS v. V = E[v/V] /\ P[v/V])[E/V]
   = (EXISTS v. E = E[v/V] /\ P[v/V])
 <== (E = E[V/V]) /\ P[V/V]
   = (E = E) /\ P
   = P


Important terminology from metatheory:

  expression
  statement
  sentence
  (first-order) theory
  soundness  |- p ==> |= p
  consistency
  completeness |= p ==> |- p
  incompleteness


Example proof:

 1. {(X+1)=3}X:=X+1{X=3}
 2. {((X+1)+1)=3}X:=X+1{(X+1)=3}
 3. {((X+1)+1)=3}X:=X+1;X:=X+1{X=3} from 1. and 2.
 4. X=1 ==> ((X+1)+1)=3
 5. {X=1}X:=X+1;X:=X+1{X=3} from 3. and 4.