Predicate transformer semantics: Difference between revisions

Revision as of 03:20, 1 December 2022

Revision as of 03:23, 1 December 2022

Line 83:

==== Total Correctness ====

To show total correctness, we also have to show that the loop terminates. For this we define a [[well-founded relation]] on the state space denoted as (wfs, <). and define a variant function '' vf '' , such that we have:

{| style="background-color:#eeeeff;" border="1" cellpadding="10"

|<math>wp(\texttt{while}\ E\ \texttt{do}\ S\ \texttt{done}, R)\ \Leftarrow \ INV \ if\ \ \ \