Skip to main content

Unit 2.3 Specifying input and output

It is crucial that one clearly specifies what the input and output conditions are for a program. In other words, it is important to assert

  • What must be true before a program starts execution. The predicate that captures this is called the precondition.

    For our program, we explicitly state that the number of terms in the polynomial, \(n \text{,}\) is nonnegative:

    \begin{equation*} 0 \leq n \end{equation*}

    We implicitly assume that \(n \) scalar coefficients \(a_0, \ldots, a_{n-1} \) and scalar value \(x \) are given.

  • What must be true after a program completes execution. The predicate that captures this is called the postcondition.

    For our program, the postcondition is given by

    \begin{equation*} y = \sum_{i=0}^{n-1} a_i x^i . \end{equation*}

We insert the precondition and postcondition at the appropriate points in our program.

We have two visual cues as to what is an assertion about the state of the variables: the curly brackets and the grey box.

Link to Logic 2.3.

Let \(S \) denote a command in our informal language. It can be a simple command like an assignment or a composite command that consist of, for example, \({\bf Algorithm~1} \text{.}\) Given command \(S \) and predicates \(P \) and \(Q \text{,}\) the Hoare triple

\begin{equation*} \left\{ P \right\} S \left\{ Q \right\} \end{equation*}

is a predicate that evaluates to true if and only the command \(S \text{,}\) when started in a state where \(P \) is true, completes in a finite amount of time in a state where \(Q \) is true. Here, \(P \) and \(Q \) are the precondition and postcondition, respectively, for the command \(S \text{,}\) which can be as complex as an entire program or as simple as a single assignment statement.

Thus, our program \(S \) for computing the given polynomial is correct if and only if

\begin{equation*} \begin{array}{l} \left\{ 0 \leq n \right\} \\ S \\ \left\{ y = \sum_{i=0}^{n-1} a_i x^i \right\} \end{array} \end{equation*}

is true. (Recall that there are implicit assumptions about \(a_{0}, \ldots, a_{n-1} \) and \(x \text{.}\))