Content deleted Content added
Line 225:
For instance, ''wp'' is artificially made strict, whereas ''wlp'' is generally not. In particular, if statement ''S'' may not terminate then
<math>wlp(S,\texttt{
:<math>wlp(\texttt{while}\ \texttt{true}\ \texttt{do}\ \texttt{skip}\ \texttt{done}, \texttt{F}) \ \Leftrightarrow \texttt{T}</math>
Indeed, '''
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, 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<ref>Chen, Wei, "Exit Statements are Executable Miracles" WUCS-91-53 (1991).
| |||