Class 31: Semantics of Assignment (2)

Held: Wednesday, 12 March 2003

Notes:

• Reminder: Extra credit for attending tomorrow's convo.
• Have a great break!
• Are there questions on exam 1?

Review

• What is a weakest precondition?
• What is substitution?
• How do we define assignment
• Notation: How should we write substitution in ASCII? How about E[x->e] for E_e^x or substitute e for x in E.

Some Problems

• wp("x = x + 1", x = x + 1)
• wp("x = a[x]", x = a[x])
• Can we simply apply the substitution rule?

Simultaneous Assignment

• Gries also defines simultaneous assignment.
• The definition looks astoundingly like that for regular assignment, except that we have vectors of variables and replacements.
  • Note that we'll need to think about how to define this kind of substitution.
• Why would we want simulataneous assignment?
• Can we redefine simultaneous assignment in terms of individual assignment?

Array Assignment

• Fairly straightforward
• Def: wp("a[x] := e", R) = x in validSubscripts(a) cand domain(e) cand R_{(a; x:e)}^x