provable in Hoare logic if and only if the predicate below hold: Usually, strongest-postconditions are used in partial correctness. Hence, we have the following relation between weakest-liberal-preconditions and strongest-postconditions: For example, on assignment we have: Above, the logical variable y represents the initial value of variable x. Hence, On sequence, it appears that sp runs forward (whereas wp runs backward): Win and sin predicate transformers Leslie Lamport has suggested win and sin as predicate transformers for concurrent programming. Predicate transformers properties This section presents some characteristic properties of predicate transformers. Below, S denotes a predicate transformer (a function between two predicates on the state space) and P a predicate. For instance, S(P) may denote wp(S,P) or sp(S,P). We keep x as the variable of the state space. Monotonic Predicate transformers of interest (wp, wlp, and sp) are monotonic. A predicate transformer S is monotonic if and only if: This property is related to the consequence rule of Hoare logic. Strict A predicate transformer S is strict iff: For instance, wp is artificially made strict, whereas wlp is generally not. In particular, if statement S may not terminate then is satisfiable. We have Indeed, T is a valid invariant of that loop. The non-strict but monotonic or conjunctive predicate transformers are called miraculous and can also be used to define a class of programming constructs, in particular, jump statements, which Dijkstra cared less about. Those jump statements include straight goto L, break and continue in a loop and return statements in a procedure body, exception handling, etc. It turns out that all jump statements are executable miracles, i.e. they can be implemented but not strict. Terminating A predicate transformer S is terminating iff: Actually, this terminology makes sense only for strict predicate transformers: indeed, is the weakest-precondition ensuring termination of S. It seems that naming this property non-aborting would be more appropriate: in total correctness, non-termination is abortion, whereas in partial correctness, it is not. Conjunctive A predicate transformer S is conjunctive iff: This is the case for , even if statement S is non-deterministic as a selection statement or a specification statement. Disjunctive A predicate transformer S is disjunctive iff: This is generally not the case of when S is non-deterministic. Indeed, consider a non-deterministic statement S choosing an arbitrary boolean. This statement is given here as the following selection statement: Then, reduces to the formula . Hence, reduces to