\documentclass[12pt]{article}
\usepackage{fullpage}
\usepackage{times}
\usepackage{enumerate}
\usepackage{amsmath,amsfonts,amssymb,amsthm}
\usepackage{fitch}
\usepackage{algorithmic}
\usepackage{algorithm}
\renewcommand{\algorithmicrequire}{\textbf{\hspace{0.5in}}}
\renewcommand{\algorithmicensure}{\textbf{\hspace{0.5in}}}
	
\newtheorem{claim}{Claim}
\newcommand{\mc}[1]{\mathcal{#1}}
\newcommand{\ignore}[1]{}

\newcommand{\hoare}[1]{(\! | #1 |\!)}
\newcommand{\num}{\mathbf{num}}
\newcommand{\ident}{\mathbf{var}}
\newcommand{\true}{\mathbf{true}}
\newcommand{\false}{\mathbf{false}}
\newcommand{\bnot}{\mathbf{not}}
\newcommand{\band}{\mathbf{and}}
\newcommand{\bor}{\mathbf{or}}
\newcommand{\bif}{\mathbf{if}}
\newcommand{\bthen}{\mathbf{then}}
\newcommand{\belse}{\mathbf{else}}
\newcommand{\bwhile}{\mathbf{while}}
\newcommand{\bdo}{\mathbf{do}}
\newcommand{\bend}{\mathbf{end}}
\newcommand{\expr}{\mathit{exp}}
\newcommand{\bool}{\mathit{bool}}
\newcommand{\command}{\mathit{code}}
\newcommand{\Inv}{\mathcal{I}}

\begin{document}

\par\noindent{\bf CS81 Notes}: {\bf Hoare Logic}

\par\noindent
We define a simple language for {\em programs} using the following grammar:
\begin{eqnarray*}
\expr & \to & 
	\num \ | \ 
	\ident \ | \ 
	- \expr \ | \
	( \expr + \expr ) \ | \ 
	( \expr - \expr ) \ | \ 
	( \expr * \expr ) \\
\bool & \to & 
	\true \ | \
	\false \ | \ 
	(\bnot \ \bool ) \ | \
	(\bool \ \band \ \bool) \ | \
	(\bool \ \bor \ \bool) \ | \
	(\expr < \expr) \\
\command & \to & 
	\ident = \expr \ | \
	\command \ ; \ \command \ | \
	\bif \ \bool \ \bthen \ \command \ \belse \ \command \ \bend \ | \
	\bwhile \ \bool \ \bdo \ \command \ \bend
\end{eqnarray*}
A {\bf Hoare triple} is a tuple consisting of
$\hoare{\alpha} C \hoare{\omega}$ 
where $\alpha$ and $\omega$ are logical formulas stating
{\em pre-condition} and {\em post-condition}, respectively,
and $C$ is a program in the form specified by the above grammar.

\paragraph{Proof Rules}
\begin{enumerate}
\item {\em Composition} (COMP) rule:
\[
\begin{nd}
\hypo {1} {\hoare{\alpha} C_{1} \hoare{\beta}}	
\hypo {2} {\hoare{\beta} C_{2} \hoare{\gamma}}
\have {3} {\hoare{\alpha} [C_{1};C_{2}] \hoare{\gamma}}
\end{nd}
\]

\item {\em Conditional} (COND) rule:
\[
\begin{nd}
\hypo {1} {\hoare{\alpha \wedge \beta} C_{1} \hoare{\omega}}	
\hypo {2} {\hoare{\alpha \wedge \lnot\beta} C_{2} \hoare{\omega}}
\have {3} {\hoare{\alpha} [\bif \ \beta \ \bthen \ C_{1} \ \belse \ C_{2} \ \bend] \hoare{\omega}}
\end{nd}
\]

\item {\em Partial-While} (LOOP) rule:
\[
\begin{nd}
\hypo {1} {\hoare{\alpha \wedge \beta} C \hoare{\alpha}}	
\have {2} {\hoare{\alpha} [\bwhile \ \beta \ \bdo \ C \ \bend] \hoare{\alpha \wedge \lnot\beta}}
\end{nd}
\]

\item {\em Assignment} (ASGN) axiom:
\[
\begin{nd}
\have {1} {\hoare{\alpha[E/x]} [x = E] \hoare{\alpha}}
\end{nd}
\]

\item {\em Consequence} (CONS) rule:
\[
\begin{nd}
\hypo {0} {\hoare{\alpha} C \hoare{\omega}}
\hypo {1} {\alpha' \vdash \alpha}	\by{pre-condition strengthening}{}
\hypo {2} {\omega \vdash \omega'}	\by{post-condition weakening}{}
\have {3} {\hoare{\alpha'} C \hoare{\omega'}}
\end{nd}
\]

\end{enumerate}


\paragraph{Example:} Proving the correctness of the following program called {\sc Fact}.
\begin{algorithmic}[1]
\STATE $y = 1$
\WHILE {$(x > 0)$}		
	\STATE $y = y * x$ ;
	\STATE $x = x - 1$
\ENDWHILE
\end{algorithmic}
The goal is to show the above program is correct.
This is equivalent to proving that the following Hoare triple holds:
\begin{equation} \label{eqn:main-triple}
\hoare{x = n \wedge n > 0} \
\mbox{\sc Fact} \
\hoare{y = n!}
\end{equation}
Let $\Inv$ be the following logical formula
\begin{equation} \label{eqn:invariant}
\Inv \equiv [x! * y = n! \wedge x \ge 0]
\end{equation}
which will be our loop invariant.
To prove that {\sc Fact} is correct, we prove that the following two triples hold:
\begin{equation} \label{eqn:init-triple}
\hoare{x = n \wedge n > 0} \ [y = 1] \ \hoare{\Inv} 
\end{equation}
\begin{equation} \label{eqn:loop-triple}
\hoare{\Inv} \ [\bwhile \ (x > 0) \ \bdo \ [y = y*x; \ x = x - 1] \ \bend ] \ \hoare{y = n!}
\end{equation}
We proceed by showing these two triples separately:
\begin{enumerate}
\item Initialization: \\
To show (\ref{eqn:init-triple}) holds, we may apply the ASGN rule:
\[
\hoare{\Inv[1/y]} \ [y = 1] \ \hoare{\Inv}
\]
But, $\Inv[1/y] = [x!=n! \wedge x \ge 0]$ and the latter is derivable from
$[x=n \wedge n > 0]$. So, by the CONS rule (pre-condition strengthening), we get
\[
\hoare{x = n \wedge n > 0} \ [y = 1] \ \hoare{\Inv}
\]

\item Loop:\\
To show (\ref{eqn:loop-triple}), we consider the following smaller substeps.
	\begin{enumerate}
	\item Body of loop:\\
	The goal is to show
	\begin{equation} \label{eqn:body-triple}
	\hoare{\Inv \wedge x > 0} \ [y = y*x; \ x = x - 1] \ \hoare{\Inv}.
	\end{equation}
	Since the body of the loop consists of a sequence of statements, we work backwards.
	Using ASGN, we get
	\[
	\hoare{\Inv_{1}} \ [x = x - 1] \ \hoare{\Inv},
	\]
	where $\Inv_{1} \equiv \Inv[(x-1)/x]$:
	\begin{equation} \label{eqn:intermediate-triple}
	\Inv_{1} = [(x-1)! * y = n! \wedge x \ge 1].
	\end{equation}
	Now, we look at the previous statement:
	\[
	\hoare{\Inv_{2}} \ [y = y * x] \ \hoare{\Inv_{1}}.
	\]
	where $\Inv_{2} \equiv \Inv_{1}[(y*x)/y]$:
	\begin{equation} \label{eqn:top-loop-triple}
	\Inv_{2} \equiv [x! * y = n! \wedge x \ge 1]. 
	\end{equation}
	From these two assertions, we have
	\[
	\hoare{\Inv \wedge x > 0} \ [y = y * x] \ \hoare{\Inv}.
	\]

	\item Test condition of loop:
	\[
	\hoare{\Inv} \ [\bwhile \ (x > 0) \ \bdo \ [y = y*x; \ x = x - 1] \ \bend \ \hoare{\Inv \wedge x \le 0}
	\]
	This follows from the LOOP rule and (\ref{eqn:body-triple}) above.

	\item Post-condition weakening:
	\[
	\hoare{\Inv} \ [\bwhile \ (x > 0) \ \bdo \ [y = y*x; \ x = x - 1] \ \bend \ ] \ \hoare{y = n!}
	\]
	This follows from the CONS rule since $(\Inv \wedge x \le 0) \vdash (y = n!)$.
	\end{enumerate}
\end{enumerate}

\newpage
\paragraph{Summary}
The preceding arguments can be summarized by the following:

\vspace{.1in}

\begin{algorithmic}[1]
\REQUIRE $\hoare{x = n \wedge n \ge 0}$ (CONS strengthening)
\REQUIRE $\hoare{x! * 1 = n! \wedge x \ge 0}$ (ASGN)
\STATE $y = 1$
\REQUIRE $\hoare{x! * y = n! \wedge x \ge 0}$ (CONS strengthening)
\WHILE {$(x > 0)$}		
	\REQUIRE $\hoare{(x-1)! * (y*x) = n! \wedge x \ge 1}$ (ASGN)
	\STATE $y = y * x$ ;
	\REQUIRE $\hoare{(x-1)! * y = n! \wedge x \ge 1}$ (ASGN)
	\STATE $x = x - 1$
	\REQUIRE $\hoare{x! * y = n! \wedge x \ge 0}$ (COMP)
\ENDWHILE
\REQUIRE $\hoare{x! * y = n! \wedge x \ge 0 \wedge x \le 0}$ (LOOP)
\ENSURE $\hoare{y = n!}$ (CONS weakening)
\end{algorithmic}
\end{document}







