3.6 Loops

We are now on our final stretch!

Let us consider algorithm 3.

$\begin{algorithm} % latex2html id marker 285\begin{algorithmic}[1] \STATE $x... ...ic} \caption{A sample prechecking (while) loop for analysis.} \end{algorithm}$

Let's begin with $% latex2html id marker 2192 $ \rm {pre(\ref{while1:while})}$$ . After the initialization of , we know that $% latex2html id marker 2196 $ \rm {pre(\ref{while1:while})} = (x = 0)$$ . However, the post condition of line 2 is not as simple. This is because there are actually two ways to get to line 2. In the first iteration, we enter from line 1. However, in subsequent iterations, we enter from line 3. On the other hand, no matter which way we come from, we know that the condition must be true if we enter the loop.

As a result, all we say at this time is that $% latex2html id marker 2200 $ \rm {post(\ref{while1:while})} = (x < 3) \wedge ((x = 0) \vee \rm {post(\ref{while1:step})})$$ . Note that $% latex2html id marker 2202 $ \rm {pre(\ref{while1:step})} = \rm {post(\ref{while1:while})}$$ .

The statement on line 3 looks familiar. It involves a function of . In this case, the inverse function is . We can then derive the following:

$% latex2html id marker 2209 $\displaystyle \rm {post(\ref{while1:step})}$$	$\displaystyle =$	$% latex2html id marker 2213 $\displaystyle \rm {sub(\rm {pre(\ref{while1:step})},x,x - 1)}$$	(17)
	$\displaystyle =$	$% latex2html id marker 2217 $\displaystyle ((x-1) < 3) \wedge (((x-1) = 0) \vee \rm {post(\ref{while1:step})})$$	(18)
	$\displaystyle =$	$% latex2html id marker 2221 $\displaystyle (x \le 3) \wedge ((x = 1) \vee \rm {post(\ref{while1:step})})$$	(19)

This is interesting because the same notation appears on the left and the right hand side of the equation. The solution is to find a definition that works in this equation. Choosing $% latex2html id marker 2223 $ \rm {post(\ref{while1:step})} = (x \le 3)$$ works. This is because $(x = 1) \vee (x \le 3)$ simplifies to $x \le 3$ because it includes the case of . Furthermore, $(x \le 3) \wedge (x \le 3)$ can also simplify to just $x \le 3$ . In conclusion, we can define $% latex2html id marker 2235 $ \rm {post(\ref{while1:step})} = (x \le 3)$$ .

How about $% latex2html id marker 2237 $ \rm {post(\ref{while1:endwhile})}$$ ? In theory, we can get there using two means. First, it is possible not to enter the loop at all. Second, we can go through the loop at least once, then exit the loop. Regardless of whether we get into the loop or not, one thing is for sure: must be false. As a result,

$% latex2html id marker 2242 $\displaystyle \rm {post(\ref{while1:endwhile})}$$	$\displaystyle =$	$% latex2html id marker 2246 $\displaystyle \neg(x < 3) \wedge (\rm {pre(\ref{while1:while})} \vee \rm {post(\ref{while1:step})})$$	(20)
	$\displaystyle =$	$\displaystyle (x \ge 3) \wedge ((x = 3) \vee (x \le 3))$	(21)
	$\displaystyle =$	$\displaystyle (x \ge 3) \wedge (x \le 3)$	(22)
	$\displaystyle =$	$\displaystyle (x = 3)$	(23)

In other words, when we exit the loop, we know that .

In its general form, a prechecking loop is as follows:

$\begin{algorithm} \begin{algorithmic}[1] \WHILE{c} \STATE block \ENDWHILE \end{algorithmic} \end{algorithm}$

$% latex2html id marker 2262 $ \rm {post(\ref{while:while})} = \rm {pre(\ref{while:in})} = c \wedge (\rm {pre(\ref{while:while})} \vee \rm {post(\ref{while:in})})$$
$% latex2html id marker 2264 $ \rm {post(\ref{while:endwhile})} = \neg c \wedge (\rm {pre(\ref{while:while})} \vee \rm {post(\ref{while:in})})$$
The trick is to find a good definition of $% latex2html id marker 2266 $ \rm {post(\ref{while:in})}$$ ! $% latex2html id marker 2268 $ \rm {post(\ref{while:in})}$$ is also called the ``loop invariant''.

The general form of a postchecking loop is as follows:

$\begin{algorithm} \begin{algorithmic}[1] \REPEAT \STATE block \UNTIL{c} \end{algorithmic} \end{algorithm}$

$% latex2html id marker 2270 $ \rm {pre(\ref{repeat:step})} = \rm {pre(\ref{repeat:repeat})} \vee \rm {post(\ref{repeat:step})}$$
$% latex2html id marker 2272 $ \rm {post(\ref{repeat:until})} = c \wedge \rm {post(\ref{repeat:step})}$$
Again, the trick is to find a good definition for $% latex2html id marker 2274 $ \rm {post(\ref{repeat:step})}$$ , it is also called the ``loop invariant''.