CS 3304: Comparative Languages
Semantics
[
Course Documents
] : [
Semantics
]
Previous
Contents
Next
Keyword Index
An Axiom for Assignment
An axiom for assignment statements
:
{Q
_{x->E}
} x := E {Q}
Substitute E for every x in Q
{ P? } x := y+1 { x > 0 } P = x > 0
_{x -> y+1}
P = y+1 > 0 P = y >= 0
Basically, "undoing" the assignment and solving for y