Predicate transformer semantics: Difference between revisions

Revision as of 00:34, 5 December 2022

Revision as of 14:03, 11 December 2022

Line 25:

* version 1:

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

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

|}

Line 31:

Provided that '' E '' is well defined, we just apply the so-called ''one-point'' rule on version 1. Then

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

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

|}