Revision as of 11:05, 2 July 2024 edit 194.61.207.70 (talk) fix pdf link for Hoare Type Theory paper ← Previous edit		Revision as of 06:55, 9 July 2024 edit undo Pascal.sotin (talk \| contribs) 1 edit m →Partial Correctness: correct display of INV and fixed link Loop INVariant Next edit →
Line 71: === While loop === ==== Partial Correctness ==== Ignoring termination for a moment, we can define the rule for the ''weakest liberal precondition'', denoted ''wlp'', using a predicate ''~~\textit{~~INV}'', called the [[~~loop~~Loop ~~\textit{~~invariant\|Loop ''INV}''ariant]], typically supplied by the programmer: {\| style="background-color:#eeeeff;" border="1" cellpadding="10" \|<math>wlp(\texttt{while}\ E\ \texttt{do}\ S\ \texttt{done}, R)\Leftarrow \ \textit{INV} \ \ \text{if} \ \

Predicate transformer semantics: Difference between revisions