[ Course Documents ] : [ Semantics ]

Previous Contents Next Keyword Index

An Axiom for Assignment

• An axiom for assignment statements:

      {Qx->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