SE 504   Formal Methods and Models
Some laws and properties of Hoare triples and the wp predicate transformer

A Hoare triple1 is an expression of the form {P} S {Q}, where P and Q are predicates (the precondition and postcondition, respectively) and S is a program (i.e., code segment). It denotes the informal proposition

Execution of S beginning in any state satisfying P is guaranteed to terminate in some state satisfying Q.

It turns out that for any S and Q, there is a weakest solution to the equation Y : {Y} S {Q}. That weakest solution is denoted by the expression wp.S.Q2 (or wp(S,Q) if you prefer the more traditional function application syntax) and is pronounced as "the weakest precondition of S with respect to Q".

Due to the Strengthening the Precondition law of Hoare triples (see below), we get the following:

Relationship between Hoare triples and wp (RHTWP):

{P} S {Q}   ≡   [P ⇒ wp.S.Q]

In words, it says that a Hoare triple is true if its precondition P is at least as strong as wp.S.Q.

General Properties/Laws of Hoare triples:

Excluded Miracle: {P} S {false}   ≡   [P ≡ false]
Intuition: It is impossible for a program's execution to terminate in a state satisfying false.
Termination: {P} S {true}   ≡   "S is guaranteed to terminate if executed beginning in a state satisfying P"
Strengthening the Precondition: [P' ⇒ P]   ⇒   ({P} S {Q} ⇒ {P'} S {Q})
Equivalently (by (3.65)), [P' ⇒ P] ∧ {P} S {Q}  ⇒  {P'} S {Q}
Intuition: Strengthening the precondition of a valid Hoare triple yields a valid Hoare triple.
Weakening the Postcondition: [Q ⇒ Q']   ⇒   ({P} S {Q} ⇒ {P} S {Q'})
Equivalently (by (3.65)), [Q ⇒ Q'] ∧ {P} S {Q}  ⇒  {P} S {Q'}
Intuition: Weakening the postcondition of a valid Hoare triple yields a valid Hoare triple.
Postcondition Conjunctivity: {P} S {Q1} ∧ {P} S {Q2}   ≡   {P} S {Q1 ∧ Q2}
Intuition: If (with respect to the same precondition) execution of S is guaranteed to terminate with Q1 being true, as well as Q2 being true, then it is guaranteed to terminate with Q1 ∧ Q2 being true. The converse of this statement also holds; hence the equivalence.
Precondition Disjunctivity: {P1} S {Q} ∧ {P2} S {Q}   ≡   {P1 ∨ P2} S {Q}
Intuition: If execution of S is guaranteed to terminate with Q being true if started with either P1 being true or P2 being true, then it is guaranteed to terminate with Q being true if started with P1 ∨ P1 being true. The converse of this statement also holds; hence the equivalence.
Postcondition Disjunctivity: {P} S {Q} ∨ {P} S {R}   ⇒   {P} S {Q ∨ R}
Intuition: If (with respect to the same precondition) execution of S is guaranteed to terminate with either Q being true or R being true, then it is guaranteed to terminate with Q ∨ R being true.
Hoare Triple
Sequential Composition:		 {P} S0; S1 {Q}   ≡   (∃R |: {P} S0 {R} ∧ {R} S1 {Q})
Consequently, {P} S0 {R} ∧ {R} S1 {Q}   ⇒   {P} S0; S1 {Q}

General Properties/Laws of wp:

Excluded Miracle:[¬wp.S.false]     (i.e., [wp.S.false ≡ false])
Distributivity of Conjunction: [wp.S.Q1 ∧ wp.S.Q2   ≡   wp.S.(Q1 ∧ Q2)]
Monotonicity: [Q1 ⇒ Q2]   ⇒   [wp.S.Q1 ⇒ wp.S.Q2]
Distributivity of Disjunction: [wp.S.Q1 ∨ wp.S.Q2   ⇒   wp.S.(Q1 ∨ Q2)]
(If S is deterministic, ⇒ above can be strengthened to ≡)
wp Sequential Composition: [wp.(S0; S1).Q   ≡   wp.S0.(wp.S1.Q)]

Properties/Laws of wp and Hoare Triples wrt program constructs

Here we present laws pertaining to wp and Hoare triples that are applicable to concrete programming constructs (such as the assignment and if-then-else commands). In each case, the law pertaining to Hoare triples can be derived from the wp law for the particular programming construct and the general RHTWP law presented above.

skip:

Take skip to be a command that, when executed, has no effect. We have

wp skip Law (WPsL): [wp.skip.Q ≡ Q]

Hoare Triple skip Law (HTsL): {P} skip {Q}   ≡   [P ⇒ Q]

Assignment:

An assignment command takes the form x := E, where x is a list of variables and E is a list (having the same length) of expressions.

wp Assignment Law (WPAL): [wp.(x := E).Q  ≡  def.E ∧ Q(x:=E)]

Hoare Triple Assignment Law (HTAL): {P} x:=E {Q}  ≡  [P ⇒ def.E ∧ Q(x:=E)]

Selection (if-then-else):

A selection command has the form if B then S else T. Abbreviating this to IF, we have

wp Selection Law (WPSL): [wp.IF.Q  ≡  (B ⇒ wp.S.Q) ∧ (¬B ⇒ wp.T.Q)]

Hoare Triple Selection Law (HTSL): {P} IF {Q}  ≡  {P ∧ B} S {Q} ∧ {P ∧ ¬B} T {Q}

Sequential Composition:

wp Sequential Composition Law (WPSCL): [wp.(S1;S2).Q  ≡  wp.S1.(wp.S2.Q)]

Hoare Triple Sequential Composition Law (HTSCL): {P} S1;S2 {Q}  ≡  {P} S1 {wp.S2.Q}

Using HTSCL, we can reason that {P} S1;S2 {Q} is true if there exists a predicate R such that both {P} S1 {R} and {R} S2 {Q} are true.

Footnotes

[1] Introduced by C.A.R. "Tony" Hoare (1934- ), the pioneering computer scientist

[2] Introduced by Edsgar Dijkstra (1930-2002), the pioneering computer scientist