# Class 35: Semantics of Conditionals

Held: Wednesday, 2 April 2003

Summary: Today we consider an interesting new form of conditional and the formal definition of that form of conditional.

Related Pages:

Due

• Gries 10.

Notes:

• Since we've gotten through most of exam 1, Friday's topic is still somewhat up in the air.

Overview:

• A New Form of Conditional.
• Formal Definition.
• Example: Max.
• Example: Largest.
• An Interesting Theorem.

## Gries-Style Conditionals

• Gries's conditionals are somewhat different from those you've encountered in most normal programming languages.
• They have the form
```if
guard1 -> S1
| guard2 -> S2
| guard3 -> S3
...
| guardn -> Sn
fi
```
• First restriction: The guards are comprehensive: At least one of the guards must hold.
• Second restriction: The statement is nondeterministic. If more the guards holds, an unpredictible one of the corresponding S's is selected.
• Here's a Gries conditional that sets m to the larger of x and y:
```if
x >= y -> m := x
| y >= x -> m := y
fi
```
• Why is this a useful way to write conditionals?

## Formalizing the Meaning of Conditionals

• We use wp to carefully define the meaning of a conditional.
• Suppose we want P after a conditional. What do we need as preconditions?
• Frist: All the guards can be successfully evaluated.
• Second: At least one of the guards holds.
• Third: For any guard that holds true, the corresponding statement guarantees the postcondition.
• Writing it more formally,
wp(if G1 | G2 ... | Gn fi, P) =
(for all 1 <= i <= n, domain(Gi))
and (exists 1 <= i <= n, Gi)
and (forall 1 <= i <= n, Gi => wp(Si, P)

## Another Example: Largest Value in an Array

• Here's some standard iterative code for computing the largest value in the array a
```guess := a[1];
i := 2;
while (i <= n)
if
guess < a[i] -> guess,i := a[i],i+1
| guess > a[i] -> i := i+1
fi
eliwh
```
• We'll focus on the conditional part,
```  if
guess < a[i] -> guess,i := a[i],i+1
| guess > a[i] -> i := i+1
fi
```
• What postcondition do we desire for each repetition?
• What precondition does that suggest for the current repetition?
• How does the formal definition help?

## An Interesting Theorem

• Sometimes, we know something about the state of the system before we enter a conditional.
• For example, if we're running a loop we know something about what we expect to be true before the next repetition.
• Here's an interesting theorem about the topic.
Suppose (Q => (for all i Bi)) and (for all i, Q and B => wp(Si, P)). Then Q => wp(if-statement, P).
• Applying the theorem.

## History

Tuesday, 7 January 2003 [Samuel A. Rebelsky]

• Created generic version to set up course.

This document may be found at `http://www.cs.grinnell.edu/~rebelsky/Courses/CS195/2003S/Outlines/outline.35.html`.