3.5 Conditional statements

Let's consider algorithm 3.5 that makes

the maximum of

and

$\begin{algorithm} \begin{algorithmic}[1] \IF{$x > y$} \STATE $z \leftarrow x$\ \ELSE \STATE $z \leftarrow y$\ \ENDIF \end{algorithmic} \end{algorithm}$

Let us express the pre and post conditions of each statement. In this case, let us not to assume any values in the variables. In other words, $% latex2html id marker 2146 $ \rm {pre(\ref{findmax:if})} = \rm {true}$$

The pre condition of line 2 is not just $\rm {true}$ . This is because the only way that we get to line 2 is that the condition must be true. Consequently, $% latex2html id marker 2152 $ \rm {pre(\ref{findmax:zgx})} = (x > y)$$ . Using the same argument, the only way we get to line 4 is that $\neg(x > y)$ , which is equivalent to saying $x \le y$ . As a result, $% latex2html id marker 2158 $ \rm {pre(\ref{findmax:zgy})} = (x \le y)$$ .

The post condition of line 2 is simply $% latex2html id marker 2160 $ \rm {post(\ref{findmax:zgx})} = \rm {pre(\ref{findmax:zgx})} \wedge (z = x) = (x > y) \wedge (z = x)$$ . Similarly, the post condition of line 4 is $% latex2html id marker 2162 $ \rm {post(\ref{findmax:zgy})} = \rm {pre(\ref{findmax:zgy})} \wedge (z = y) = (x \le y) \wedge (z = y)$$ .

Here comes the trickly part: what is $% latex2html id marker 2164 $ \rm {post(\ref{findmax:endif})}$$ ? In other words, after the entire conditional statement, what can we conclude?

There are two ways to get to line 5. We can get there from line 2, or from line 4. Consequently, the post condition of line 5 is the post condition of line 2 or the post condition of line 4. In other words,

$% latex2html id marker 2167 $\displaystyle \rm {post(\ref{findmax:endif})}$$	$\displaystyle =$	$% latex2html id marker 2171 $\displaystyle \rm {post(\ref{findmax:zgx})} \vee \rm {post(\ref{findmax:zgy})}$$	(15)
	$\displaystyle =$	$\displaystyle ((x > y) \wedge (z = x)) \vee ((x \le y) \wedge (z = y))$	(16)

Does this make sense?

Here is the general conditional statement:

$\begin{algorithm} \begin{algorithmic}[1] \IF{c} \STATE then-block \ELSE \STATE else-block \ENDIF \end{algorithmic} \end{algorithm}$

$% latex2html id marker 2177 $ \rm {pre(\ref{genif:then})} = \rm {pre(\ref{genif:if})} \wedge c$$
$% latex2html id marker 2179 $ \rm {pre(\ref{genif:else})} = \rm {pre(\ref{genif:if})} \wedge \neg c$$
$% latex2html id marker 2181 $ \rm {post(\ref{genif:then})}$$ has no general form, it depends on the actual code of ``then-block''. Note that even may not true after the code of ``then-block''.
$% latex2html id marker 2185 $ \rm {post(\ref{genif:else})}$$ has no general form, it depends on the actual code of ``else-block''. Note that may actually be true after the code of ``else-block''.
$% latex2html id marker 2189 $ \rm {post(\ref{genif:endif})} = \rm {post(\ref{genif:then})} \vee \rm {post(\ref{genif:else})}$$