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?