The definition of weakest precondition for a non-deterministic language

In the classical IMP language, the definition of weakest precondition is:

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

This is stating that from state s, after executing c we get to a state satisfying Q. My question comes when handling the IF FI construct in the language of guarded commands (see selection command in Wikipedia). My guess is that in this case one needs to define:

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

I wonder if this is correct and whether it is the standard way of writing it in the literature.

Currently, I'm having problems proving the weakest precondition definition for the sequential composition of commands:

"wp (c1;;c2) Q s = wp c1 (wp c2 Q) s"

So, I'm beginning to think my definition is wrong. Quoting wikipedia:

the result of this function, denoted wp(S,R), is the "weakest" precondition on the initial state ensuring that execution of S terminates in a final state satisfying R.

so termination is required in the definition, and this is not properly imposed so far. There could be non-terminating branches.

• The last $t$ in your definition should be a $t'$.
– Kai
Feb 21 '19 at 22:18

First of all, the definition of weakest precondition you've mentioned might be a little bit confusing. Namely, remember that the weakest precondition, designates all states of a program, such that when the given command executes, the given postcondition is satisfied.

Therefore, your initial definition might be a bit confusing, in the sense that the weakest precondition wp(s, Q) is determined really based on a postcondition (which you have as Q) and a command (which you have a c) -- that is all that is needed to define weakest precondition (w.p.).

Having that said, a more natural definition of wp(c, Q) says that: $$wp(c, Q) = \{ \sigma \in \Sigma | \text{ex}[c, \sigma] \models Q \}$$ the weakest precondition, given c and Q, is a set of all states, such that executing c (denoted simply by ex here) from those states, assuming the execution terminates (we will come back to that later), will lead to some state $$\sigma$$ for which the postcondition Q is satisfied.

Given that, the weakest precondition you've mentioned, namely

"wp (c1;;c2) Q s = wp c1 (wp c2 Q) s"

is a valid formulation for w.p. for compositions, as, naturally, executing c1 you want to end up in a state belonging to the weakest precondition of wp(c2, q), which, in turn, means that after further executing c2 (in the sequence) you will have to satisfy postcondition (again, with the assumption that both terminate).

Now, in terms of this weakest precondition formulation, while the quote

ensuring that execution of S terminates in a final state satisfying R

might confuse you, this does not say that termination is encoded in the w.p. formulation. Specifically, it is not required: the definition of weakest precondition says, that, if the given command executes and terminates, from those states, the postcondition has to hold.

That is why this is part of something traditionally called "partial correctness" and not "total correctness", as it does not prescribe termination (but rather, effectively, works under assumption of termination).

• 1. wp does imply termination. wikipedia
– Kai
Feb 21 '19 at 22:05
• 2. your "more natural definition" amounts to wp c Q s ≡ ∀ t. (c,s) ⇒ t ⟶ Q t) in Javier's notation, simply omitting the first conjunct. That conjunct is crucial if there are commands $c$ that do not produce any final state for some initial state in the "⇒" semantics.
– Kai
Feb 21 '19 at 22:17
• Well not quite. Nevertheless, there is a notion of "partial correctness" (the traditional verification, and most commonly implied one) and "total correctness" -- the former does not imply termination and verification techniques are effectively completely orthogonal to total correctness. Feb 23 '19 at 22:03
• I don't see how the alternative definition brings any value. Commands are always best explained by intuitively defining execution to change the state of the program. (Perhaps you can expand on this with some practical example -- but it seems you can define special program states for the special cases of "no state".) Feb 23 '19 at 22:09