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:

• EBoard.

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
  

• You can think about this as a special collection of if statements with some restrictions.
• 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 G₁ | G₂ ... | G_n fi, P) =
     (for all 1 <= i <= n, domain(G_i))
     and (exists 1 <= i <= n, G_i)
     and (forall 1 <= i <= n, G_i => wp(S_i, P)

An Example: Maximum of Two Values

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 B_i)) and (for all i, Q and B => wp(S_i, P)). Then Q => wp(if-statement, P).

• Applying the theorem.