Given a set 
of states and a program C, the weakest liberal precondition of
C and W is defined as
Usually S will be denoted by a logical expression Q, so we set correspondingly
For a straight line program C and a logical expression Q, wlp(C,Q) is again definable by a logical expression :
If C is a while-loop, wlp(C,Q) need not be first order definable. Notice that according to our characterization of the while-loop as a countable sequence of conditionals, we can always write it as a countable disjunction
where 
is the straight line program consisting of the n-fold iteration
of the command `` 
''.