# Class 30: Semantics of Assignment (1)

Back to Designing a List Type. On to Semantics of Assignment (2).

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:

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
• Eex 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 Rex
• 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)
= x2 > 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)

## History

Tuesday, 7 January 2003 [Samuel A. Rebelsky]

• Created generic version to set up course.

Tuesday, 11 March 2003 [Samuel A. Rebelsky]

• Filled in lots of details.

Back to Designing a List Type. On to Semantics of Assignment (2).

Disclaimer: I usually create these pages on the fly, which means that I rarely proofread them and they may contain bad grammar and incorrect details. It also means that I tend to update them regularly (see the history for more details). Feel free to contact me with any suggestions for changes.

This document was generated by Siteweaver on Fri May 2 14:20:46 2003.
The source to the document was last modified on Tue Mar 11 14:01:56 2003.
This document may be found at `http://www.cs.grinnell.edu/~rebelsky/Courses/CS195/2003S/Outlines/outline.30.html`.

You may wish to validate this document's HTML ; ; Check with Bobby

Samuel A. Rebelsky, rebelsky@grinnell.edu