Content deleted Content added
Line 226:
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{false})</math> is satisfiable. We have
:<math>wlp(\texttt{while}\ \texttt{true}\ \texttt{do}\ \texttt{skip}\ \texttt{done}, \texttt{
Indeed, '''true''' 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, 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"
https://openscholarship.wustl.edu/cse_research/671</ref>, i.e. they can be implemented but not strict.
| |||