Predicate transformer semantics: Difference between revisions

Revision as of 17:38, 2 December 2022

Revision as of 00:34, 5 December 2022

Line 150:

|}

It combines Morgan's syntactic idea with the sharpness idea by Bijlsma, Matthews and Wiltink.<ref>Chen, Wei and Udding, Jan Tijmen, "The Specification Statement Refined" WUCS-89-37 (1989).

https://openscholarship.wustl.edu/cse_research/749</ref>. The very advantage of this is its capability of defining wp of goto L and other jump statements. <ref>Chen, Wei, "A wp Characterization of Jump Statements," 2021 International Symposium on Theoretical Aspects of Software Engineering (TASE), 2021, pp. 15-22. doi: 10.1109/TASE52547.2021.00019.</ref>

=== Goto statement ===

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, 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,<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.

=== Terminating ===