Predicate transformer semantics: Difference between revisions

Revision as of 11:30, 29 November 2022

Revision as of 11:31, 29 November 2022

Line 236:

:<math>S(\texttt{T})\ \Leftrightarrow\ \texttt{T}</math>

Actually, this terminology makes sense only for strict predicate transformers: indeed, <math>wp(S,\texttt{trueT})</math> 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.