Use of Pre- and Postconditions

Peter Müller

August 26, 1998

Using Conditions to Proove Correctness

Pre- and postconditions can be used to proove algorithms for correctness. I will show this with a small example. Since the course is no course on formal programming theory, this will only give you a first glance on this subject. However, since abstract data types are so important for object-oriented programming, I thought it useful to introduce them.

Consider the following code fragment which calculates the sum of the first 10 whole numbers:

$\begin{tabular} {lll} \textbf{INTEGER} i; & &\\ \textbf{INTEGER} n; & &\\ \textb... ...$\quad$\space i $\leftarrow$\space i + 1; & &\\ \textbf{END} & &\\ \end{tabular}$

We will now show with pre- and postconditions that this loop really calculates the sum. However, I will only give and explain those conditions which are of interest here. Just before we enter the loop, the following precondition hold:

$\begin{equation} \left\{ s = 0 = \sum^{i-1}_{j=1}j \quad \mbox{and} \quad i \le n \right\}\end{equation}$

I use the notation $\sum^{n}_{i=1}i$ to denote the sum over all numbers from 1 to n. Note that $\sum^{0}_{i=1}i$ is defined to be 0. (We use this in the above loop precondition!)

Since the loop condition holds (i $\le$ n) we can enter the loop. Until now, we have:

$\begin{tabular} {lll} \textbf{INTEGER} i; & &\\ \textbf{INTEGER} n; & &\\ \textb... ...$\quad$\space i $\leftarrow$\space i + 1; & &\\ \textbf{END} & &\\ \end{tabular}$

The next statement is the increment of s by the value of i. Using the precondition, this would yield to

$\begin{equation} \left\{ s = \sum^{i-1}_{j=1}j \:+\: i \quad \mbox{and} \quad i \le n \right\}\end{equation}$

This can be simplified to:

$\begin{equation} \left\{ s = \sum^{i}_{j=1}j \quad \mbox{and} \quad i \le n \right\}\end{equation}$

The next line increments i by 1. What does this mean to the current precondition? Well, just that the value of i has changed! As a consequence, every occurrence of i must be adopted to reflect this change, leading to the following postcondition of the i assignment:

$\begin{equation} \left\{ s = \sum^{i-1}_{j=1}j \quad \mbox{and} \quad i-1 \le n \right\}\end{equation}$

The second part of this condition can be rewritten as:

$\begin{eqnarray*} i-1 \le n & \Rightarrow & i \le n+1 \\ & \Rightarrow & i < n+... ...= n+1\\ & \Rightarrow & i \le n \quad \mbox{or} \quad i = n+1\\ \end{eqnarray*}$

Note that the first term (i $\le$ n) is exactly the loop condition. If this term evaluates to true, the body is executed again. However, the conditions hold each time the loop body is executed. They are invariant regarding the execution.

Only if the second part is true, the loop terminates. So after the loop the following condition holds:

$\begin{equation} \left\{ s = \sum^{i-1}_{j=1}j \quad \mbox{and} \quad i=n+1 \right\}\end{equation}$

From this, we can conclude:

$\begin{eqnarray*} s = \sum^{i-1}_{j=1}j \quad \mbox{and} \quad i=n+1 & \Rightarrow & s = \sum^{n}_{j=1}j\end{eqnarray*}$

With the fact that n equals 10 we have shown, that the loop really do what we have expected.

Finally, the whole loop with all conditions is shown:

$\begin{tabular} {lll} \textbf{INTEGER} i; & &\\ \textbf{INTEGER} n; & &\\ \textb... ...uad i=n+1 \:\Rightarrow\: s=\sum^{n}_{j=1}j \right\} $\space & &\\ \end{tabular}$

About this document ...

Use of Pre- and Postconditions

This document was generated using the LaTeX2HTML translator Version 97.1 (release) (July 13th, 1997)

The command line arguments were:
latex2html -html_version 3.0 -split +0 -show_section_numbers -no_navigation -t Pre- and Postconditions -antialias -toc_stars -local_icons -dir conditions main.tex.

The translation was initiated by P. Mueller on 8/26/1998

P. Mueller
8/26/1998