Predicate transformer semantics: Difference between revisions

Revision as of 18:32, 29 November 2022

Revision as of 18:33, 29 November 2022

Line 25:

* version 1:

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

|<math> wp(x := E, R)\ =\ (\forallexits y : y = E : R(x \leftarrow y))</math>

where ''y'' is a fresh variable and not free in E and R (representing the final value of variable ''x'')

|}