Predicate transformer semantics: Difference between revisions

Revision as of 09:16, 25 November 2024

Latest revision as of 09:17, 25 November 2024

Line 201:

For example, on assignment we have:

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

|<math> sp(x := E, R)\ =\ \exists y, x=E[x \leftarrow y] \wedge R[x \leftarrow y]</math>

where ''y'' is fresh

Line 211:

On sequence, it appears that ''sp'' runs forward (whereas ''wp'' runs backward):

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

|<math>sp(S_1;S_2\ ,\ R)\ =\ sp(S_2,sp(S_1,R))</math>

|}