The Law of Excluded Miracle in the language of guarded commands

Question

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

according to this article the meaning of this proposition would be:

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?

Answer 1

The answer I can provide is I was reusing the definition of weakest precondition from the IMP language, but in fact I need a stronger definition. This definition looks as follows:

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

It is taking care of non-determinism. When one evaluates:

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

One realizes that the statement is simply saying that the program either terminates, or does not terminate. Therefore, the import point now is to see whether my proposed definition is correct or can be improved in any way.