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.