\documentstyle{6.170-ps}

\def\d#1{d$_{#1}$}
\newcommand{\ol}[1]{\multicolumn{3}{l}{#1}}
\newcommand{\imp}{\hskip1ex$\Longrightarrow$\hskip1ex}
\newenvironment{proof}{\begin{tabular}{c}}{\end{tabular}}
\newenvironment{proof3}{\begin{tabular}{rcl}}{\end{tabular}}

\psnum{4}
\duedate{Wednesday, November 29, 1989}
\handedoutdate{Thursday, November 16, 1989}
\handoutnumber{\strut}
\pstitle{Program Verification}
\name{Marc Horowitz}
\date{Wednesday, November 29, 1989}
\TARF

\begin{document}
\maketitle
\centerline{\large Marc Horowitz}

initial assertion: x $>$ 0

Proof of assignment: \\
\verb+y := x+

\begin{proof}
\begin{proof3}
& x $>$ 0 & \\
\{ & y := x & \} \\
& (y $>$ 0) \& (x = y)
\end{proof3} \\ \hline
x $>$ 0 \imp (x $>$ 0) \& (x = x) \\ \hline
TRUE
\end{proof}

Proof of assignment: \\
\verb+z := 0+

\begin{proof}
\begin{proof3}
& TRUE & \\
\{ & z := 0 & \} \\
& z = 0 
\end{proof3} \\ \hline
TRUE \imp 0 = 0 \\ \hline
TRUE
\end{proof}

Proof of while loop:

\begin{verbatim}
while y < 0 do
   y := y - 2
   z := z + 1
   end
\end{verbatim}

loop invariant: 2 * z = x - y \\
decrementing function: \d{n} = y over the range y $\geq$ -1

\fbox{P \imp Inv}

\begin{proof3}
(y $>$ 0) \& (z = 0) \* (x = y) & \imp & 2 * z = x - y \\ \hline
(y $>$ 0) \& (z = 0) \* (x = y) & \imp & 0 = 0 \\ \hline
\ol{TRUE}
\end{proof3}

\fbox{Inv \{b\} Inv}

\begin{proof}
\begin{proof3}
& 2 * z = x - y & \\
\{ & y $>$ 0 & \} \\
& 2 * z = x - y 
\end{proof3} \\ \hline
2 * z = x - y \imp 2 * z = x - y \\ \hline
TRUE
\end{proof}

\fbox{Inv \& b \{S\} Inv}

\begin{proof}
\begin{proof3}
& (2 * z = x - y) \& (y $>$ 0) & \\
\{ & y := y - 2 & \\
& z := z + 1 & \} \\
& (2 * z = x - y) 
\end{proof3} \\ \hline
\begin{proof3}
& (2 * z = x - y) \& (y $>$ 0) & \\
\{ & y := y - 2 & \} \\
& (2 * (z + 1) = x - y) 
\end{proof3} \\ \hline
\begin{proof3}
(2 * z = x - y) \& (y $>$ 0) & \imp & (2 * (z + 1) = x - y + 2) \\ \hline
(2 * z = x - y) \& (y $>$ 0) & \imp & (2 * z + 2 = x - y + 2) 
\end{proof3} \\ \hline
TRUE
\end{proof}

\fbox{(Inv \& $\neg$ b) \imp Q}

\begin{proof}
(2 * z = x - y) \& (y $\leq$ 0) \imp (2 * z = x - y) \\ \hline
TRUE
\end{proof}

\fbox{{\bf while} b {\bf do} S {\bf end} terminates}

Decrementing function is decremented by the body:

\begin{proof}
\begin{proof3}
& (y = \d{0}) \& (y $>$ 0) & \\
\{ & y := y - 2 & \\
& z := z + 1 & \} \\
& y $<$ \d{0} 
\end{proof3} \\ \hline
\begin{proof3}
& (y = \d{0}) \& (y $>$ 0) & \\
\{ & y := y - 2 & \} \\
& y $<$ \d{0}
\end{proof3} \\ \hline
(y = \d{0}) \& (y $>$ 0) \imp y - 2 $<$ \d{0} \\ \hline
TRUE
\end{proof}

Test does not increment decrementing function:

\begin{proof}
\begin{proof3}
& y = \d{0} & \\
\{ & y $>$ 0 & \} \\
& y $\leq$ \d{0}
\end{proof3} \\ \hline
y = \d{0} \imp y $\leq$ \d{0} \\ \hline
TRUE
\end{proof}

When decrementing function reaches -1, the loop terminates:

\begin{proof}
(y = -1) \imp y $\leq$ 0 \\ \hline
TRUE
\end{proof}

Proof of conditional: \\
\verb+if y = 0 then isEven := true else isEven := false end+

\fbox{side-effect-free(b)}

\begin{proof}
side-effect-free(y $>$ 0) \\ \hline
TRUE
\end{proof}

\fbox{P \& b \{s1\} Q}

\begin{proof}
\begin{proof3}
& (2 * z = x - y) \& (y $\leq$ 0) \& (y $\geq$ -1) \& (y = 0) & \\
\{ & isEven := TRUE & \} \\
& isEven = (2 * z = x)
\end{proof3} \\ \hline
(2 * z = x - y) \& (y $\leq$ 0) \& (y $\geq$ -1) \& (y = 0) \imp
TRUE = (2 * z = x) \\ \hline
TRUE
\end{proof}

\fbox{P \& $\neg$ b \{s2\} Q}

\begin{proof}
\begin{proof3}
& (2 * z = x - y) \& (y $\leq$ 0) \& (y $\geq$ -1) \& (y $\neq$ 0) & \\
\{ & isEven := FALSE & \} \\
& isEven = (2 * z = x) 
\end{proof3} \\ \hline
(2 * z = x - y) \& (y $\leq$ 0) \& (y $\geq$ -1) \& (y $\neq$ 0) \imp
FALSE = (2 * z = x) \\ \hline
TRUE
\end{proof}

Final assertion: isEven = (2 * z = x)

\large{QED}
\end{document}
