Predicate transformer semantics: Difference between revisions

Revision as of 22:17, 21 April 2023

Revision as of 10:24, 19 May 2023

Line 25:

* version 1:

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

|<math> wp(x := E, R)\ =\ (\existsforall 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'')

|}