Content deleted Content added
Pascal.sotin (talk | contribs) m →Partial Correctness: correct display of INV and fixed link Loop INVariant |
m →While loop: Sentence casing for sub-section titles, as per WP:STYLE. |
||
Line 70:
=== While loop ===
==== Partial
Ignoring termination for a moment, we can define the rule for the ''weakest liberal precondition'', denoted ''wlp'', using a predicate ''INV'', called the [[Loop invariant|Loop ''INV''ariant]], typically supplied by the programmer:
{| style="background-color:#eeeeff;" border="1" cellpadding="10"
Line 82 ⟶ 83:
|}
==== Total
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 ({{mvar|wfs}}, <) and define a variant function {{mvar|vf}} , such that we have:
{| style="background-color:#eeeeff;" border="1" cellpadding="10"
| |||