What is a predicate transformer?
The predicate transformer is just a formalization of the idea that you can produce a precondition given a program and its postcondition.

For example, given a program sqrt with the postcondition that sqrt(x) = y and y*y = x, what are some valid preconditions?


x > 10
x > 20
x > 1


Some invalid preconditions would be


x &lt; 0
x > -10


One predicate P1 is weaker than another predicate P2 if P2 =&gt; P1, but it is not true that P1 =&gt; P2. For example, x &gt; 1 is weaker than x &gt; 10 because x &gt; 10 implies x &gt; 1 as well, but x &gt; 1 does not imply x &gt; 10; x == 3 would be a counterexample.

Given all possible preconditions for our square-root program, one must be the weakest of them all; we denote that with the function wp.S.Q (which you could also write in the more familiar notation wp(S, Q)). In this case, wp.S.Q = {x &gt;=0 }. You can prove that if x satisfies any precondition P, then it must satisfy x &gt;= 0, and that if it does not satisfy x &gt;= 0, it cannot satisfy any other precondition P.

The idea of a weakest precondition is useful because it allows a program to work with as many values as possible. Using a precondition of x &gt;= 20 isn't useful because it doesn't allow us to compute the square root of 4.

Note that just because wp.S.Q is defined, that doesn't mean we have to provide an algorithm to actually compute its value. Doing so would provide a constructive proof of its existence, but non-constructive proofs could be found as well.