Class 30: Semantics of Assignment (1)

Held: Tuesday, 11 March 2003

Summary: Today we consider the definition of a variety of assignment statements using weakest preconditions as a definition technique.

Related Pages:

• EBoard.

Due

• Gries 9.

Notes:

• Extra credit for attending the Marlene Zuk convocation or 4:15 lecture on Thursday (double extra credit for attending both).
• Did anyone solve the muddy children problem?
• Are there questions on exam 1?

Overview:

• Review: Weakest Preconditions.
• Review: Substitution.
• Defining simple assignment.
• Some variations.
• Defining multiple assignment.

Some Background

• Our goal for today is to carefully define some particular forms of assignment.
• In order to do so, we'll need to review two key topics we've covered, explicitly or implicitly.
  • Weakest preconditions.
  • Substitution.

Weakest Preconditions

• The predicate transformer wp is a function of two parameters.
  • A statement in the language we're defining.
  • A desired postcondition.
• The postcondition is a predicate.
  • Recall that a predicate represents a set of states.
• The result of wp is a precondition.
• s is in statesOf(wp(S,P) if transform(s,S) is in statesOf(P).
  • The transform operation represents changes to a state based on a statement.
• It's weakest in the sense that any other set of states is smaller.
• We typically use wp to define statements.

Substitution

• In our definition of the assignment statement, we'll need to rely on the substitution operation.
• You can find the definition of that operation informally on p. 80 of Gries
• E_e^x denotes substitute e for x in E.
• We replace every free occurrence of x in E by e.
• If the replacement causes variables in e to become bound, we must do renaming.
• Can anyone give an example of the latter happening?

Semantics of Simple Assignment

• Def: wp("x := e", R) = domain(e) cand R_e^x
• What does the domain reflect?
• Why are we using cand rather than and?
• Why are we doing substitution backwards?

Some Simple Examples

• wp("x = 5", x > 4)
  = 5 > 4
  = true
  This always holds.
• wp("x = 1", x > 4)
  = 1 > 4
  = false
  This never holds.
• wp("x = y", x > 4)
  = y > 4
• wp("x = x*x", x > 4)
  = x² > 4
  = (x > 2) or (x < -2)
• wp("x = a[i]", x > 4)
  = i in validSubscripts(a) cand a[i] > 4
• wp("x = a[i]", x = a[i])
  = i in validSubscripts(a) cand a[i] = a[i]
  = i in validSubscripts(a)

A Stranger Example

• wp("x = a[x]", x = a[x])
• Can we simply apply the substitution rule?
• Is this an instance of a badly designed postcondition, as in
  wp("x = x + 1", x = x + 1)