typo in ch4, Section 4.1.1. first formula

[alexioslyrakis]

This is a typo in ch4, Section 4.1.1. first formula.

[AllanBlanchard]

Hum, no this is not a typo. The formula is either $$wp(x = E , Post) := Post[x \leftarrow E]$$ or $$wp(x = E , P) := P[x \leftarrow E]$$. Here, I first talk about Post, and then explain what this notation means for any property P.

[alexioslyrakis]

Oh I see, so the latter example P = wp(x = 43 * c, {x = 258}) could also be written as {x = 258}[x <- 43 * c] ?

[AllanBlanchard]

Exactly

[alexioslyrakis]

Thanks, all this notation is new to me and it's a bit tricky :) I close the request