\documentclass{slides}

\usepackage{amsmath}
\usepackage{latexsym}
\usepackage{amssymb}
% \usepackage{exptrees}

\newenvironment{heading}{\noindent\centering\large\bf}{\par}
\newenvironment{Heading}{\noindent\centering\Large\bf}{\par}

\begin{document}

\input{defs}

\begin{slide}
  \begin{Heading}
  {Formalizing General Correctness}
  \end{Heading}

\begin{center}
\begin{tabular}{c}
\normalsize Jeremy Dawson \\
\mbox{} \\
{Automated Reasoning Group and} \\
{Dept.\ of Computer Science} \\
{Australian National University} \\
{Canberra, Australia} \\
\mbox{} \\
{\tt jeremy@csl.anu.edu.au} \\
\end{tabular}

Supported by an ARC Large Grant

\end{center}
\end{slide}

\begin{slide}
  \begin{heading}
  {Formalizing General Correctness}
  \end{heading}

Based on Steve Dunne's abstract commands, 
which is based on Jacobs \& Gries semantics.

$\wp (A, P)$ -- ``weakest precondition'', 
condition on state that command $A$ will
terminate in new state satisfying $P$ 

$\trm(A)$ -- ``termination condition'',
condition on state that command $A$ will terminate

$\wlp (A, P)$ -- ``weakest liberal precondition'',
condition on state that if command $A$ terminates, it will
do so in new state satisfying $P$ 

$$\wp (A, P)\ s = \trm(A)\ s \land \wlp (A, P)\ s$$
Note: non-determinism is allowed, so
$$\wlp (A, P)\ s \not= \trm(A)\ s \to \wp (A, P)\ s$$

\end{slide}

\begin{slide}
\begin{heading}
{Refinement - $A$ refines $B$}
\end{heading}
Partial correctness : $\forall Q\ s. \wlp (A, Q)\ s \to \wlp (B, Q)\ s$

Total correctness : $\forall Q\ s. \wp (A, Q)\ s \to \wp (B, Q)\ s$

General correctness : both above are satisfied

\begin{heading}
Specifying abstract commands (Dunne)
\end{heading}
eg, sequencing ``$A; B$'', $\land$ lifted over state $s$
$$\wlp (A;B, Q) = \wlp(A, \wlp (B, Q))$$
$$\trm (A;B) = \trm (A) \land \wlp(A, \trm (B))$$
\end{slide}

\begin{slide}
  \begin{Heading}
  {Operational Semantics}
  \end{Heading}

\begin{verbatim}
datatype outcome = NonTerm | Term state

types
  cmdMeaning = "state => outcome set"
  expMeaning = "state => nat"
  bexpMeaning = "state => bool"

consts
  seq      :: "[cmdMeaning, cmdMeaning] =>
      cmdMeaning"
  guard    :: "bexpMeaning => cmdMeaning =>
      cmdMeaning"


\end{verbatim}
\end{slide}

\begin{slide}
  \begin{Heading}
  {Monads}
  \end{Heading}

So when we model sequencing of two commands $A$ and $B$, we first
apply $A$ to a given state, obtaining a set of outcomes, and we must then
apply $B$, a function of type 
$$\state \to \outcome\ \set$$ 
to the set of outcomes obtained from $A$.
We can think of this as ``extending'' the function $B$ to a function of type
$$\outcome\ \set \to \outcome\ \set$$
When this can be done in a way that satisfies certain conditions,
we call the relationship between the types a \textbf{monad}.
\end{slide}

\begin{slide}

  \begin{heading}
  {A Compound Monad}
  \end{heading}

In fact, this is an example of a \emph{compound monad}.
The type \outcome, relative to the type \state, is a monad,
where the extension function, 
of type $$(\state \to \outcome) \to (\outcome \to \outcome)$$ would be given by
\begin{eqnarray*}
exto\ f\ \texttt{NonTerm} & = & \texttt{NonTerm} \\
exto\ f\ (\texttt{Term}\ s) & = & f s 
\end{eqnarray*}

For any type $\alpha$, the type $\alpha\ \set$ (the type of sets of things of
type $\alpha$) is also a monad,
where the extension function, 
of type 
$$(\alpha \to \alpha\ \set) \to (\alpha\ \set \to \alpha\ \set)$$
would be given by
\begin{eqnarray*}
exts\ f\ os & = & \bigcup_{o \in os} f\ o 
\end{eqnarray*}

\end{slide}

\begin{slide}
  \begin{heading}
  {Its Extension Function}
  \end{heading}
Here is the extension function for the compound monad, of type
\begin{eqnarray*}
\lefteqn{(\state \to \outcome\ \set) \to} \\
 & & (\outcome\ \set \to \outcome\ \set)
\end{eqnarray*}
$
\begin{array}{lllll}
\multicolumn{5}{l}{extos\ f\ os\ =} \\
 \qquad & let & f'\ (\texttt{Term}\ s) & = & f\ s \\
 & & f'\ \texttt{NonTerm} & = & units\ \NonTerm \\
  & \multicolumn{4}{l}{in\ exts\ f'\ os}
\end{array}
$

$
\begin{array}{lllll}
\multicolumn{5}{l}{extos\ f\ os\ =} \\
 \qquad & let & f'\ (\texttt{Term}\ s) & = & f\ s \\
 & & f'\ \texttt{NonTerm} & = & \{\NonTerm\} \\
  & \multicolumn{4}{l}{in\ \bigcup_{o \in os} f'\ o}
\end{array}
$

Then define sequencing of commands by
$$(A; B)\ s = extos\ B\ (A\ s)$$
\end{slide}

\begin{slide}

\begin{Heading}
{Meaning of Commands} 
\end{Heading}
\begin{heading}
eg, Guarded command
\end{heading}

The command $P \longrightarrow A$ is the same as $A$ if $P$ holds,
but is infeasible if $P$ does not hold.

Dunne's definition: ($\to$ lifted over $s$)
$$\trm (P \longrightarrow A) = P \to \trm (A)$$
$$\wlp (P \longrightarrow A, Q) = P \to \wlp (A, Q)$$

Our definition:
\begin{verbatim}
guard ?P ?A ?s == if ?P ?s then ?A ?s else {}
\end{verbatim}

Using Isabelle, we prove, from our definitions,
the \wlp\ and termination conditions for commands
(which Dunne uses to \emph{define} these commands)
\end{slide}

\begin{slide}

\begin{Heading}
{Meaning of Refinement} 
\end{Heading}
We proved characterizations of refinement
\begin{eqnarray*}
{\texttt{totcref}\ A\ B } 
  & = & \forall s. B\ s \subseteq A\ s \lor \NonTerm : A\ s \\
{\texttt{partcref}\ A\ B } 
  & = & \forall s. B\ s \subseteq \{\NonTerm\} \cup A\ s \\
\texttt{gencref}\ A\ B & = &  
  \forall s. B\ s \subseteq A\ s
\end{eqnarray*}

Note how that for general correctness is simpler than the other two.
This explains some of the advantages of working with general correctness,
as outlined by Dunne.

\end{slide}

\begin{slide}

\begin{Heading}
{Issues}
\end{Heading}

\begin{itemize}
\item
Assignment rule % (similar in Hoare logic):
$$\wlp (x := E, Q) = Q[x := E] 
%\qquad \{P[x := E]\}\  x := E \ \{Q\}
$$
Substituting in $Q$ means $Q$ not just function $\state \to \bool$
but term of a defined language (eg the command language \
\textit{plus} logical variables -- Gordon).

\item
But to \textit{prove} this rule from operational definition,
can only prove it as equality of functions $\state \to \bool$

\item
Paper addresses other tricky issues arising from Dunne's formulation.
\end{itemize}


\end{slide}

\begin{slide}

\begin{Heading}
{Free Iteration}
\end{Heading}

$\repall\ A$ is the (unbounded) choice of any number of repetitions of
$A$.
The termination condition for $\repall\ A$ is that for every
$n$, $A^n$ terminates.

The \emph{free iteration} of $A$ is $A^{*}$, where the outcomes
of $A^{*}$ are those of \repall, augmented by 
\NonTerm\ in the case where it is feasible to execute $A$
infinitely many times sequentially.

It is considerably easier to define this concept operationally 
than in terms of \wlp\ and \trm.

Dunne defines both $\trm(A^*)$ and $\wlp(A^*, Q)$ as fixpoints:
\begin{eqnarray*}
\trm(A^*) & = & \nu Y. \wp(A, Y) \\
\wlp(A^*, Q) & = & \mu Y. \wlp(A, Y) \land Q
\end{eqnarray*}
and he also defines $A^*$ itself as a least fixpoint under the
\emph{Egli-Milner} refinement relation 
$$A^* \equiv \mu_{em} X. (A ; X) \Box \skp$$

\end{slide}
\end{document}