Predicate transformer semantics: Difference between revisions

Revision as of 10:24, 19 May 2023

Revision as of 13:13, 19 May 2023

Line 25:

* version 1:

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

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

|}