3
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Kai Feb 2 at 8:06
3
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.