Predicate transformer semantics: Difference between revisions

Revision as of 11:58, 29 November 2022

Revision as of 11:59, 29 November 2022

Line 157:

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

|<math>wp(goto\ \ L, R) = wpL</math>

where ''wpL'' is the weakest precondition at label ''L''.

|}