Predicate transformer semantics: Difference between revisions

Revision as of 03:32, 1 December 2022

Revision as of 17:38, 2 December 2022

Line 232:

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., Inin 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<ref>Chen, Wei, "Exit Statements are Executable Miracles" WUCS-91-53 (1991).

https://openscholarship.wustl.edu/cse_research/671</ref>, i.e. they can be implemented but not strict.