Examples

Consider the following Hoare triples.

1. \( \{x < 0\} \; c \; \{(x = 1) \vee (x = 2)\} \)
2. \( \{x > 0\} \; c \; \{(x = 0) \vee (x = -1)\} \)
3. \( \{x > 1\} \; c \; \{x < 0\} \)

What transitions are possible from a state in which \(x = -1\) by a command \(c\) that satisfies all the above three Hoare triples?

Since the state satisfies the first precondition, \(x < 0\), the state after the transition must satisfy the first postcondition, \((x = 1) \vee (x = 2)\). The other two Hoare triples don't address the precondition \(x = -1\), and so the postconditions of these Hoare triples are irrelevant for this question. Therefore, the transitions from \(x = -1\) are to states \(x = 1\) or \(x = 2\).

Example

What transitions are possible from a state in which \(x = 2\) that satisfy all of the above Hoare triples?

The first Hoare triple doesn't address the precondition \(x = 2\).

The precondition \(x > 0\) of the second triple holds when \(x = 2\) and therefore its postcondition, \((x = 0) \vee (x = -1)\), must hold in the next state.

The precondition \(x > 1\) of the third triple holds when \(x = 2\) and therefore its postcondition, \(x < 0\), must hold in the next state.

Both postconditions, \((x = 0) \vee (x = -1)\) and \(x < 0\) must hold in the next state. So the only transition from \(x = 2\) is to state \(x = -1\).

Example

What transitions are possible from a state in which \(x = 0\)?

None of the three preconditions hold when \(x = 0\), and therefore the next state can be any state.

Example: Unimplementable Commands

What transitions satisfy all the following Hoare triples?

\( \{x = 0\} \; c \; \{x > 0\}, \quad \{x = 0\} \; c \; \{x < 0\} \)

This command cannot be initiated in a state in which \(x = 0\) because both postconditions \(x > 0\) and \(x < 0\) must hold when the command terminates.

In this course we will ensure that the commands specified in our algorithms can be executed in every state.

Summary

We may specify a command by sets of pre- and post-conditions that the command must specify. There may be many commands that satisfy these conditions, and we can use any command that satisfies these conditions in an implementation. Specifying commands in this way allows us to describe algorithms in terms of predicates rather than by using statements in a specific programming language.

---

K. Mani Chandy, Emeritus Simon Ramo Professor, California Institute of Technology