
\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} % Slide 1
  \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.Dawson@nicta.com.au} \\
\end{tabular}

Supported by an ARC Large Grant

\end{center}
\end{slide}

\begin{slide} % Slide 2
  \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} % Slide 3
\begin{heading}
{Refinement - $A$ refines $B$}
\end{heading}
Partial correctness : \\
\mbox{} \quad $\forall Q\ s.\ \wlp (A, Q)\ s \to \wlp (B, Q)\ s$

Total correctness : \\
\mbox{} \quad $\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} % Slide 4
  \begin{Heading}
  {Operational Semantics}
  \end{Heading}

\begin{verbatim}
datatype outcome = NonTerm | Term state
\end{verbatim}
We use set-valued functions for commands \\
(equivalent to relations)
\begin{verbatim}
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} % Slide 5
  \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} % Slide 6

  \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} % Slide 7
  \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} % Slide 8

\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} % Slide 9

\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 the one for general correctness is simpler than the other two. \\
This explains some advantages of working with general correctness,
outlined by Dunne, \\ eg monotonicity of the abstract commands.

Also proved that general correctness refinement distinguishes 
commands which are operationally different.
$$\texttt{gencref}\ A\ B \land \texttt{gencref}\ B\ A \Rightarrow A = B$$
\end{slide}

\begin{slide} % Slide 10
\begin{Heading}
{Strongest Postconditions}
\end{Heading}

$$\slp (A, Q)\ s' = \exists s.\ Q\ s \land \texttt{Term}\ s' \in A\ s$$

Analogous to \wlp\ -- changing $A$ to (dis)allow extra possibility of
non-termination does not change \slp.

Define \slp-refinement as 
$$\forall Q\ s. \slp (B, Q)\ s \to \slp (A, Q)\ s$$
We proved \slp-refinement = \wlp-refinement 

Galois connection between \wlp\ and \slp\
$$Q \longrightarrow \wlp\ C\ R \Longleftrightarrow
  \slp\ C\ Q \longrightarrow R$$

\wp\ does not have a Galois dual
\end{slide}

\begin{slide} % Slide 10
\begin{heading}
{Strongest postconditions using outcomes}
\end{heading}

However we can define strongest post- and weakest pre-conditions based on
\emph{outcomes}, and these are Galois duals.
\begin{eqnarray*}
C & : & \state \to \outcome\ \set \\
\spom\ C & : &
(\state \to \bool) \to \outcome\ \to \bool\ \\
\wpom\ C & : & 
(\outcome\ \to \bool) \to \state \to \bool\ \\
\end{eqnarray*}
\vspace{-7ex}
\begin{eqnarray*}
\spom\ C\ Q\ c &=& \exists s.\ Q\ s \land c \in C\ s \\
\wpom\ C\ R\ s &=& \forall c \in C\ s.\ R\ c
\end{eqnarray*}
Note that $R$ is a predicate on outcomes, $Q$ on states.

\end{slide}
\begin{slide} % Slide 10

\begin{Heading}
{Assignment Rule}
\end{Heading}

% Assignment rule % (similar in Hoare logic):
\begin{center}
$\wlp (x := E, Q) = Q[x := E] 
%\qquad \{P[x := E]\}\  x := E \ \{Q\}
$
\end{center}

Requires $Q$ to be not just a function $\state \to \bool$
but a term of a defined language (eg the command language \
\textit{plus} logical variables -- Gordon).
But to \textit{prove} this rule from operational definition,
can only prove it as equality of functions $\state \to \bool$

We defined this language (datatype \aexp), 
and meaning and substitution functions \\
\texttt{expMng} : $\aexp \to \state \to \val$ \\
\texttt{expSub} : $\name \to \aexp \to \aexp \to \aexp $

Other possible approach: \emph{define} $ Q[x := E]$ by
$$Q[x := E] s \equiv Q (s[x := E])$$
(where the type \state\ is $\name \to \val$)

We \emph{proved} this equality from our definitions
\begin{verbatim}
"expMng (expSub ?x ?E ?Q) ?state =
  expMng ?Q (?state(?x := expMng ?E ?state))"
\end{verbatim}


\end{slide}

\begin{slide} % Slide 11

\begin{Heading}
{Repetition \& 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.

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 least fixpoint under the
\emph{Egli-Milner} refinement relation 
$$A^* \equiv \mu_{em} X. (A ; X) \Box \skp$$

It is considerably easier to define this concept operationally 
than in terms of \wlp\ and \trm. 
We then \emph{prove} Dunne's characterisations.

\end{slide}

\begin{slide} % Slide 11

\begin{Heading}
{The \while\ Loop}
\end{Heading}

Operationally, programmers define

$ \while\ G\ \ddo\ A\ \eend  \ \equiv\ $ \\
  $\mbox{}\qquad \iif\ G\ \then\ A ; \while\ G\ \ddo\ A\ \eend\ \eend$

We cannot use this as a definition in Isabelle since it is recursive --
as it stands it is non-terminating, and when applied to a particular state,
may not terminate.

Dunne defines
\begin{eqnarray*}
\iif\ G\ \then\ A\ \eend & \ \equiv\ & (G \to A) \Box (\lnot G \to \skp) \\
\while\ G\ \ddo\ A\ \eend & \ \equiv\ & (G \to A)^* ; \lnot G \to \skp
\end{eqnarray*}

In Isabelle define $\while$ as Dunne -- we proved
that it satisfies the operational definition.

\end{slide}

\begin{slide} % Slide 11

\begin{Heading}
{Indeterminate Assignment}
\end{Heading}
for $x$ a (list of) variables \\
$P$ a relation (\emph{old-state, new-state}) \\
$x : P$ assigns values to $x$ satisfying $P$

\begin{verbatim}
indetass ?vars ?P ?s == 
  Term ` (Collect (?P ?s) Int chst ?vars ?s)
\end{verbatim}

Lermer, Fidge \& Hayes give \wlp\ and \sp
(adapted)
($x'$ is post-value(s) of $x$, $Q$ involves $x$ \emph{and} $x'$)
\begin{eqnarray*}
\wlp (x:Q, R) &=& \forall x'. Q \to R[x := x'] \\
\sp (x:Q, R) &=& (\exists x. R \land Q)[x' := x]
\end{eqnarray*}
What does $\exists x. \ldots$ mean exactly?

``for some values $x$,
which, when taken to be the values of variables $x$, \ldots''
($x$ overloaded)

\end{slide}

\begin{slide} % Slide 11

\begin{heading}
{Indeterminate Assignment in Isabelle}
\end{heading}
\begin{eqnarray*}
\wlp (x:Q, R) &=& \forall x'. Q \to R[x := x'] \\
\sp (x:Q, R) &=& (\exists x. R \land Q)[x' := x]
\end{eqnarray*}

$\texttt{setvars} : \name\ \set \to \state \to \state \to \state $
$\texttt{setvars}\ x\ s'\ s = s[x := s']$
\begin{verbatim}
"wlpm (indetass ?x ?Q) ?R ?s =
  (ALL s'. (?s, setvars ?x s' ?s) : ?Q -->
    ?R (setvars ?x s' ?s))"

"slpm (indetass ?x ?Q) ?R ?s' =
  (EX s. (setvars ?x s ?s', ?s') : ?Q &
    ?R (setvars ?x s ?s'))"
\end{verbatim}

\end{slide}

\begin{slide} % Slide 11

\begin{Heading}
{Block Structure -- $@z. A$}
\end{Heading}
$z$ a new ``local'' variable in $A$

Model this command as follows:

 (1) set variables $z$ to arbitrary values, using \texttt{setvars} \\
 (2) execute $A$ \\
 (3) reset $z$ to initial values, using \texttt{revert}

\begin{verbatim}
revert ?z ?A ?s ==
   mapos (setvars ?z ?s) (?A ?s)
at ?z ?A ?s ==
   let setz = %s'. setvars ?z s' ?s;
      szA = %x. UNION UNIV (?A o setz)
   in revert ?z szA ?s
\end{verbatim}

Here, $\texttt{UNION UNIV}\ F = \bigcup_x F \;x$,
and \texttt{mapos} is the monadic ``map'' function:
% $\texttt{mapos} \;f\; \textit{ocset} =
  % \{\textit{mapo} \;f\; s \;|\; s \in \textit{ocset} \}$, where
\begin{eqnarray*}
\textit{mapos} \;f\; \textit{ocset} & = &
  \{\textit{mapo} \;f\; s \;|\; s \in \textit{ocset} \} \\
\textit{mapo} \;f\; (\texttt{Term} \;s) & = & \texttt{Term} \;(f \;s) \\
\textit{mapo} \;f\; \texttt{NonTerm} & = & \texttt{NonTerm}
\end{eqnarray*}

\end{slide}

\begin{slide} % Slide 11

\begin{Heading}
{$\wlp$ and $\sp$ for $@z. A$}
\end{Heading}

\begin{verbatim}
"trmm (at ?z ?A) = allvars ?z (trmm ?A)"
\end{verbatim}
where \texttt{allvars z} $B\ s$
means that $B$ holds after
setting the variables \texttt{z} to any values.
$$\texttt{allvars}\ z\ B\ s = \forall x. B (s[z := x])$$

Tried to prove
$\wlp\ (@z. A, Q) = \forall z.\ \wlp\ (A, Q)$ (Dunne)
but overlooked his assumption -- $Q$ does not involve $z$.
We proved 
\begin{verbatim}
"wlpm (at ?z ?A) ?Q ?s = (ALL x. wlpm ?A 
  (?Q o setvars ?z ?s) (setvars ?z x ?s))"
"slpm (at ?z ?A) ?Q ?s = (EX x. slpm ?A 
  (?Q o setvars ?z ?s) (setvars ?z x ?s))"
\end{verbatim}
\end{slide}

\begin{slide} % Slide 11

\begin{Heading}
{Formulae for $\wlp$ and $\sp$}
\end{Heading}

Lermer, Fidge \& Hayes (adapted)
\begin{eqnarray*}
\wlp (@z. A, Q) & = & (\forall z. \wlp\ (A, Q[z := y]))[y := z] \\
\sp (@z. A, Q) & = & (\exists z. \sp\ (A, Q[z := y]))[y := z]
\end{eqnarray*}
where $y$ denotes new variables which do not appear (free) in $A$ or $Q$.

To reconcile these:
\begin{eqnarray*}
\lefteqn{(\forall z. \wlp\ (A, Q[z := y]))[y := z] s} \\
  &=& (\forall z.\ \wlp\ (A, Q\circ \setvars\ z\ y))[y := z] s \\
  &=& \forall x.\ (\wlp\ (A, Q\circ \setvars\ z\ y) \circ \\
  & & \qquad \setvars\ z\ x)[y := z] s \\
  &=& \forall x.\ \wlp\ (A, Q\circ \setvars\ z\ s) (\setvars\ z\ x\ s)
\end{eqnarray*}
\end{slide}

\begin{slide} % Slide 11

\begin{Heading}
{Simplifying $@z. A$ ??}
\end{Heading}
Using \texttt{revert} is messy.
We tried to reflect reality better, with

(1) map from variable names to memory locations \\
(2) map from memory locations to values

Entry and exit to/from inner blocks pushes/pops (1)
(though changing only for $z$); leaves (2) unchanged.

This turned out \emph{more} complex, especially \\
  -- stating freshness of new memory locations \\
  -- specifying equivalence of states \\
and was abandoned. 

\end{slide}
\end{document}
