# The Law of Excluded Miracle in the language of guarded commands

The definition of weakest precondition is familiar (let me use Isabelle's syntax here):

definition "wp c Q s ≡ ∃t. (c,s) ⇒ t ∧ Q t"


the weakest precondition ensuring Q when executing a command in an initial state s is given by the formula in the RHS.

Now, Dijkstra, for instance in, "Nondeterminacy and Formal Derivation of Programs" talks about the law of the excluded middle:

definition "F ≡ λ t. False"

lemma "wp c F = F" unfolding wp_def F_def by simp


started in a given state, a program execution must either terminate or loop forever

However, I don't see how this proposition states this fact. Unrolling the definitions I get:

∃t. (c,s) ⇒ t ∧ (λ t. False) t = ∃t. (c,s) ⇒ t ∧ False = False


seen as a function in s, obviously this LHS matches the RHS. However, I don't see how this tells that the program terminates or loops. Could you explain what is happening here?

• Dijkstra's GCL has non-deterministic language constructs whereas IMP doesn't. That's why you shouldn't use IMP's definition of wp for GCL. Since Dijkstra's formulated his laws, things have changed. Nowadays, we're quite happy with "miraculous" commands because they make the refinement algebra nicer. Check the Morgan's Programming from Specifications, Chapter 23 for details and the rest of the book for motivation. – Kai Feb 2 at 8:06

definition "wp c Q s ≡ (∃t. (c,s) ⇒ t) ∧ (∀ t'. (c,s) ⇒ t' ⟶ Q t')"

lemma excluded_miracle: "wp c (λ t. False) = (λ s. False)"