\documentclass[a4,12pt]{seminar}

\usepackage{latexsym}
\usepackage{pstricks}
\usepackage{pst-node}
\usepackage{epsf}
\usepackage{float}
\usepackage{amssymb}
\usepackage{comment}
\usepackage{semlayer}

\usepackage{talk}

\input{../memoire/macros/macros-gen.tex}
\input{../memoire/macros/macros-terms.tex}
\input{../memoire/macros/macros-effects.tex}
\input{../memoire/macros/macros-logic.tex}

\newcommand{\correctbleu}[3]{{\bleu\{#1\}}~#2~{\bleu\{#3\}}}

\psset{unit=0.3cm}
\psset{nodesep=0.2cm}

\begin{document}

\sf

\begin{slide}{}
  \pagestyle{empty}
  \begin{center}
    {\navyblue\rule{\linewidth}{0.5mm}} \\[0.7em]
    {\Large\navyblue Verifying Imperative Programs with Coq} \\
    {\navyblue\rule{\linewidth}{0.5mm}} \\[2em]
    {\large\monvert Jean-Christophe Filli\^atre}\\[0.7em]
    {\large\monvert SRI International} \\[3em]
    % {\monvert LRI, Orsay, France} \\[0.2em]
    % {\monvert www.lri.fr/\unixtilde filliatr} \\[2em]
    {\large Kestrel Institute, \today}
  \end{center}
\end{slide}          

\begin{slide}
  \slidehead{Overview}
  \begin{enumerate}
  \item Constructive proofs and extraction \medskip
  \item How to deal with imperative programs \medskip
  \item The tactic Correctness \medskip
  \item Case studies \medskip
  \item Comparisons with other works
  \end{enumerate}
  \vfill
\end{slide}


%%%% 1. extraction %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{slide}{}
  \slidehead{Constructive proofs and Extraction}
  Coq implements a \remph{constructive} logic, the Calculus of
  Inductive Constructions
  \vfill
  A proof of $\exists x.P(x)$ is an explicit witness $n$ together
  with a proof of $P(n)$
  \vfill
  From each proof, one can extract a \remph{program} corresponding to the
  informative part
  \vfill
\end{slide}

\begin{slide}{}
  \slidehead{Programs Extraction (C. Paulin, 89)}
  \vfill
  % positionnement et paramètres
  %\vspace*{1.2cm}
  \hspace*{1cm}
  % situation initiale : extraction
  \rput(0,0){\rnode{preuve}{$\pi : \forall x.P(x) 
      \Rightarrow \exists y.Q(y)$}}
  \rput(30,0){\rnode{extraction}{${\cal E}(\pi) : X \rightarrow Y$}}
  \ncline{->}{preuve}{extraction}
  \Aput{Extraction}
  % réalisabilité
  \rput(15,-6){realizability : $\forall x. P(x) \Rightarrow Q({\cal
      E}(\pi)(x))$}
  \vfill
\end{slide}

\newcommand{\id}[1]{\textrm{\textit{#1}}}

\begin{slide}{}
\slidehead{Example}
\small
\begin{flushleft}
Inductive \id{Even} : nat $\rightarrow$ Prop := \\
~~  | \id{EvenO} : (\id{Even} O)                          \\
~~  | \id{EvenS} : (\id{n}:nat)(\id{Odd} \id{n}) $\rightarrow$ (\id{Even} (S \id{n}))    \\
with \id{Odd} : nat $\rightarrow$ Prop :=                       \\
~~  | \id{OddS} : (\id{n}:nat)(\id{Even} \id{n}) $\rightarrow$ (\id{Odd} (S \id{n})).    \\
\bigskip
Lemma \id{even\_odd} :                                    \\
~~  \mbox{(\id{n}:nat) {\red\{} \id{b}:bool {\red| (\id{b}=true $\land$
  (\id{Even} \id{n})) $\lor$ (\id{b}=false $\land$ (\id{Odd} \id{n})) \}}}. \\
Proof.                                          \\
Induction n.                                    \\
...
\end{flushleft}
\end{slide}

\begin{slide}{}
\slidehead{Example (cont'd)}
\small
  \begin{flushleft}
    Require Extraction. \\
    Write Caml File "\texttt{even\_odd}" [\textit{even\_odd}]. \\[-0.2cm]
  \end{flushleft}
  \medskip
  \tt\scriptsize
  \begin{flushleft}
    {\blue\hrulefill}\\[-0.1cm]
    {\blue\texttt{even\_odd.ml}}\\[-0.2cm]
    {\blue\hrulefill}\\
    type bool = True | False \\

    type nat = O | S of nat \\

    let even\_odd n = \\
    ~~let rec f1 = function \\
    ~~~~ O $\rightarrow$ True \\
    ~~| S n1 $\rightarrow$ (match f1 n1 with  True $\rightarrow$ False
    | False $\rightarrow$ True) \\
    ~~in f1 n \\[-0.1cm]
    {\blue\hrulefill}
  \end{flushleft}
\end{slide}

\begin{slide}{}
  \slidehead{The tactic Program (C. Parent, 95)}
  \vfill
  % positionnement et paramètres
  \vspace*{1.2cm}
  \hspace*{1cm}
  % situation initiale : extraction
  \rput(0,0){\rnode{preuve}{$\pi : \forall x.P(x) 
      \Rightarrow \exists y.Q(y)$}}
  \rput(30,0){\rnode{extraction}{$\begin{array}{l}{\rouge f} : X
      \rightarrow Y\end{array}$}} 
  \ncline{->}{preuve}{extraction}
  \Aput[0.3cm]{Extraction}
  % réalisabilité
  \rput(15,-6){realizability : $\forall x. P(x) \Rightarrow 
      Q({\rouge f}(x))$}
  % thèse de Catherine
  \rput(0,10){\rnode{preuvep}{${\rouge\chape{\pi}} : \forall x.P(x) 
      \Rightarrow \exists y.Q(y)$}}
  \ncarc{<-}{extraction}{preuvep}
  %\Aput{Extraction}
  \ncarc[linecolor=rouge]{<-}{preuvep}{extraction}
  \Aput{{\rouge Program}}
  \ncline{->}{preuvep}{preuve}
  \Bput{\parbox{2.3cm}{resolution \par of obligations}}
  \vfill
\end{slide}

\begin{comment}
\begin{slide}{}
  \slidehead{Example}
  \begin{flushleft}
Lemma \id{even\_odd\_prog} : \\
~~  (\id{n}:nat) \{ \id{b}:bool | (\id{b}=true $\land$ (\id{Even} \id{n})) \\
~~~~~~~~~~~~~~~~~~~~~~~$\lor$ (\id{b}=false $\land$ (\id{Odd} \id{n})) \}. \\
\medskip
Realizer Fix \id{prog} \{ \id{prog} [\id{n}:nat] : bool := \\
~~~~~~~~~~~Cases \id{n} of \\
~~~~~~~~~~~~~O $\Rightarrow$ true \\
~~~~~~~~~~~| (S \id{p}) $\Rightarrow$ if (\id{prog} \id{p}) then false else true end \\
~~~~~~~~~~~end \}. \\
Program\_all. \\
...
  \end{flushleft}
\end{slide}

\begin{slide}{}
  \slidehead{Proof obligations}
  \begin{displaymath}
    \irule{}{(\mbox{true}=\mbox{true}\land\mbox{(\id{Even} O)})  ~\lor~ 
      (\mbox{true=false}\land\mbox{(\id{Odd} O)})}
  \end{displaymath}
  \vfill
  \begin{displaymath}
    \irule{(\mbox{true=true}\land\mbox{(\id{Even} \id{p})}) ~\lor~ 
      (\mbox{true=false}\land\mbox{(\id{Odd} \id{p})})}
          {(\mbox{false=true}\land\mbox{(\id{Even} (S \id{p}))}) ~\lor~
            (\mbox{false=false}\land\mbox{(\id{Odd} (S \id{p}))})}
  \end{displaymath}
  \vfill
  \begin{displaymath}
    \irule{(\mbox{false=true}\land\mbox{(\id{Even} \id{p})}) ~\lor~
      (\mbox{false=false}\land\mbox{(\id{Odd} \id{p})})}
          {(\mbox{true=true}\land\mbox{(\id{Even} (S \id{p}))}) ~\lor~
            (\mbox{true=false}\land\mbox{(\id{Odd} (S \id{p}))})}
  \end{displaymath}
  \vfill
\end{slide}
\end{comment}

%%%% 2. Interprétation fonctionnelle des pgms imp. %%%%%%%%%

\begin{slide}{}
  \slidehead{What about imperative programs?}

  Two main issues
  \begin{itemize}
  \item how to \remph{specify} the programs? \par
    $\Rightarrow$ Floyd-Hoare logic \bigskip

  \item how to \remph{establish the correctness}? \par
    $\Rightarrow$ functional interpretation i.e. denotational semantics
    
  \end{itemize}
\end{slide}

\begin{slide}{}
  \slidehead{Our approach}
  \vfill
  % positionnement et paramètres
  \vspace*{1.2cm}
  \hspace*{1cm}
  % situation initiale : extraction
  \rput(0,0){\rnode{preuve}{$\pi : \forall x.P(x) 
      \Rightarrow \exists y.Q(y)$}}
  \rput(27,0){\rnode{extraction}{${\bleu\barre{e}} : X \rightarrow Y$}}
  \ncline{->}{preuve}{extraction}
  \Aput[0.5cm]{Extraction}
  % réalisabilité
  \rput(15,-6){realizability : $\forall x. P(x) \Rightarrow
    Q({\bleu\barre{e}}(x))$} 
  % ma contribution
  \rput(0,10){\rnode{preuvep}{${\bleu\chape{e}} : \forall x.P(x) 
      \Rightarrow \exists y.Q(y)$}}
  \ncline{<-}{extraction}{preuvep}
  \rput(27,10){\rnode{programme}{\bleu $\correct{P}{e}{Q}$}}
  \ncline[linecolor=bleu]{->}{programme}{preuvep}
  \Bput{{\bleu partial proof}}
  \ncline[linecolor=bleu]{->}{programme}{extraction}
  \Aput{\parbox{5cm}{{\bleu functional \par translation}}}
  \ncline{->}{preuvep}{preuve}
  \Bput{\parbox{2.3cm}{resolution \par of obligations}}
  \vfill
\end{slide}

\begin{slide}
  \slidehead{A natural interpretation}
  Denotational semantics traditionally interprets imperative programs
  as \remph{stores} transformers

  \medskip
  This is not natural, and not suitable for reasoning about programs

  \medskip
  We expect references to be interpreted as functional variables
\end{slide}

\newcommand{\pgms}{%
    \begin{tabular}{l|l}
      % C program
      \begin{minipage}[t]{5cm}
        \vspace{-1cm}\begin{program}
          i = 0; \\[-0.2em]
          \kw{while} ~ (i < n) ~ \{ \rnode{A}{\phantom{A}} \\[-0.2em]
          ~~~ \kw{if} ~ (p(a[i])) ~ \{ ~ \kw{break}; ~ \} \\[-0.2em]
          ~~~ i\textsf{\small++} ; \\[-0.2em]
          \} 
        \end{program}
      \end{minipage}
      &
      % ML program
      \begin{minipage}[t]{5cm}
        \vspace{-1cm}\begin{program}
          \kw{let rec} ~ \mathit{lookup} ~ i ~ = \rnode{B}{} \\[-0.2em]
          ~~~ \kw{if} ~ i = n ~ || ~ (p ~ a.[i]) ~ \kw{then} ~ i \\[-0.2em]
          ~~~ \kw{else} ~ \mathit{lookup} ~ (i+1) \\[-0.2em]
          \kw{in} \\[-0.2em]
          \mathit{lookup} ~ 0 
        \end{program}
      \end{minipage}
    \end{tabular}}

\begin{slide}
  \slidehead{Example}
  \begin{center}
    \pgms
    \\[2em]
    \phantom{{\red $\forall j. ~ 0 \leqslant j < i \Rightarrow \lnot p(a[j])$}}
  \end{center}
\end{slide}

\begin{slide}
  \slidehead{Example (cont'd)}
  \begin{center}
    \pgms
    \\[2em]
    {\red\rnode{C}{$\forall j. ~ 0 \leqslant j < i \Rightarrow \lnot p(a[j])$}}
    \ncline[nodesep=3pt,linecolor=red]{->}{C}{A}
    \ncline[nodesep=3pt,linecolor=red]{->}{C}{B}
  \end{center}
\end{slide}

\begin{slide}
  \slidehead{Effects}
  Standard \remph{typing with effect} \`a la Talpin \& Jouvelot
  \begin{displaymath}
    \Gamma \vdash e : (\tau,\epsilon)
  \end{displaymath}
  \medskip
  Effects are sets of read and write variables $\epsilon = (\rho,\omega)$
  \medskip
  \begin{displaymath}
    \begin{array}{llcl}
      \mbox{values}       & \tau   & ::= & 
             \beta \sep \reftype{\beta} \sep (x:\tau) \rightarrow \kappa
      \\
      \mbox{computations} & \kappa & ::= & (\tau,\epsilon)
    \end{array}
  \end{displaymath}
\end{slide}

\begin{slide}
  \slidehead{Aliases}
  Aliases are \remph{excluded}

  \medskip
  \begin{displaymath}
    f \quad\equiv\quad \kw{fun} ~ x ~ y \rightarrow 
           \aff{x}{!x+1}; ~ \aff{y}{!y+1}
  \end{displaymath}
  \begin{displaymath}
    \vdash (f ~ r) : (y:\reftype{\kw{int}}) \rightarrow (\kw{unit},\{r,y\})
  \end{displaymath}
  \smallskip
  \begin{displaymath}
    \mbox{but} \quad ((f ~ r) ~ r) \quad \mbox{cannot be typed}
  \end{displaymath}
  \medskip\small
  \begin{displaymath}
    \irule{\Gamma \vdash e :
           ((x:\reftype{\tau_1})\rightarrow(\tau_2,\epsilon_2), \epsilon)
           \qquad
           r : \reftype{\tau_1} \in \Gamma
           \qquad
           r \not\in (\tau_2,\epsilon_2)}
          {\Gamma \vdash (e ~ r) : (\tau_2[x\leftarrow r],
           \epsilon\sqcup\epsilon_2[x\leftarrow r])}
  \end{displaymath}
\end{slide}

\newcommand{\opg}[2]{\mu_{#1}\,#2}
\renewcommand{\unitg}[2]{\kw{unit}_{#1,#2}}
\renewcommand{\starg}[2]{\kw{star}_{#1,#2}}
\begin{slide}
  \slidehead{Monads parameterized by effects}

  Usual \remph{state monads} are too coarse ($\mu~\tau \equiv S
  \rightarrow S \times \tau$)
  \begin{displaymath}
    \begin{array}{lcl}
      \kw{unit} & : & \tau \rightarrow \mu~\tau\\
      \kw{star} & : & \mu~\tau \rightarrow (\tau \rightarrow
                      \mu~\tau') \rightarrow \mu~\tau'
    \end{array}
  \end{displaymath}

  \medskip
  We introduce a notion of \remph{monads parameterized by effects}.
  $\opg{\epsilon}{\tau}$ represents a computation of type $\tau$ and
  effect $\epsilon$
  \begin{displaymath}
    \begin{array}{lcl}
      \unitg{\epsilon_1}{\epsilon_2} & : & 
      \opg{\epsilon_1}{\tau} \rightarrow \opg{\epsilon_2}{\tau} \\
      \starg{\epsilon_1}{\epsilon_2}  & : &
      \opg{\epsilon_1}{\tau} \rightarrow 
        (\tau \rightarrow \opg{\epsilon_2}{\tau'})
        \rightarrow \opg{\epsilon_1\sqcup\epsilon_2}{\tau'}
    \end{array}
  \end{displaymath}
\end{slide}

\begin{slide}{}
  \slidehead{The main steps}
  \begin{enumerate}
  \item annotated program \quad $\correct{P}{e}{Q}$
  
  \item type and effect inference \quad 
  $\vdash e : (\tau, \epsilon)$ 

  with $\epsilon = (\{x_1,\dots,x_n\},\{y_1,\dots,y_m\})$

  \item functional translation \\
  $\barre{e} : \mu_\epsilon~\tau = X_1\times\cdots\times X_n \rightarrow
     Y_1\times\cdots\times Y_m\times T$ 
  
  \item goal $\forall\vec{x}. ~ P(\vec{x}) \Rightarrow \exists
  \vec{y},v. ~ Q(\vec{x}, \vec{y}, v)$ 

  refined using a partial proof term built upon $\barre{e}$
  \end{enumerate}
\end{slide}

\begin{slide}
  \slidehead{Example}
  
  \begin{program}
    {\red\{ ~ (\mathit{Even}~n) ~ \}} \\[-0.2em]
    n ~ := ~ !n \,/\, 2; \\[-0.2em]
    k ~ := ~ !k + 1; \\[-0.2em]
    {\red\{ ~ n\cdot 2^k = \avant{n}\cdot 2^{\scriptsize\avant{k}} ~ \}}
  \end{program}%

  \begin{program}
    \lambda (n,k). ~ {\red\lambda h:(\mathit{Even}~n)}. \\[-0.2em]
    ~~~~~~~~~~~~~~~ \mlletin{n_1}{n / 2}{} \\[-0.2em]
    ~~~~~~~~~~~~~~~ \mlletin{k_1}{k+1}{} \\[-0.2em]
    ~~~~~~~~~~~~~~~ ((n_1,k_1),\kw{void},{\red?:n_1\cdot 2^{k_1} = n\cdot 2^k})
  \end{program}%
\end{slide}

\begin{slide}
  \slidehead{The proof obligation}
  After reduction of the proof term, we get

  \begin{displaymath}
    \begin{array}{l}
      n, k : \kw{nat} \\
      h : (\mathit{Even}~n) \\
      \hline
      n/2\cdot 2^{k+1} = n\cdot 2^k
    \end{array}
  \end{displaymath}
\end{slide}

\begin{comment}
\begin{slide}{}
  \slidehead{Example}
  \small
  \begin{flushleft}
  Global Variable \id{n} : nat ref. \\
  \medskip
  Correctness \id{even\_odd\_imp} \\
~~~~(let \id{b} = ref true in \\
~~~~~while !\id{n} $\not=$ 0 do \\
~~~~~~~\red\{ invariant \id{n} $\le$ \id{n}$^0$ $\land$ ((\id{b}=true $\land$ (\id{Even} (\id{n}$^0$-\id{n}))) \\
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ $\lor$ (\id{b}=false $\land$ (\id{Odd} (\id{n}$^0$-\id{n})))) \\
~~~~~~~~~variant \id{n} for \id{lt} \} \black \\
~~~~~~~\id{n} := !\id{n} - 1; \\
~~~~~~~if !\id{b} then \id{b} := false else \id{b} := true \\
~~~~~done; !\id{b}) \\
~~~~{\red\{ (result=true $\land$ (\id{Even} \id{n}$^0$)) $\lor$ (result=false
  $\land$ (\id{Odd} \id{n}$^0$)) \}}. \\
  \end{flushleft}
\end{slide}

\begin{slide}{}
  \slidehead{Typing and functional interpretation}
  $$\vdash \id{even\_odd\_imp} : (\id{bool}, \{n\})$$
  \vfill
  $$\barre{\id{even\_odd\_imp}} : \mbox{nat} \rightarrow \mbox{nat}
  \times \mbox{bool}$$
  \vfill
  $$\forall n^0. ~ \exists n,b. ~ 
  (b=\mbox{true}\land (\mbox{\id{Even}}~n^0)) \lor
  (b=\mbox{false}\land(\mbox{\id{Odd}}~n^0))$$ 
  \vfill
\end{slide}

\begin{slide}{}
  \slidehead{Five proof obligations}
  $$\irule{I(n,b), ~ 0<n}{n-1<n}$$
  \vfill
  $$\irule{I(n,b), ~ 0<n, ~ b=\mbox{true}}{I(n-1,\mbox{false})} \qquad
    \irule{I(n,b), ~ 0<n, ~ b=\mbox{false}}{I(n-1,\mbox{true})}$$
  \vfill
  $$\irule{}{I(n^0,\mbox{true})} \qquad
    \irule{I(n,b), ~ n=0}{Q(b)}$$
  \vfill
\end{slide}
\end{comment}

%%% results

\begin{slide}
  \slidehead{Correctness}
  {\em If the partial proof term is completed (i.e. if the obligations
  are proved) then the program terminates and satisfies the specification.}
\end{slide}

\begin{slide}  
  \slidehead{Completeness}
  {\em If the program terminates and satisfies its specification, then
  it can be annotated in such a way that all the obligations are provable.}

  \bigskip
  (loops and recursive functions are not considered here)
\end{slide}

%%%% 3. la tactique Correctness %%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{slide}{}
  \slidehead{The tactic Correctness}
  \begin{itemize}
  \item The programming language
  \item The specifications
  \item The proof obligations
  \end{itemize}
\end{slide}

\begin{slide}{}
  \slidehead{The programming language}
  \begin{itemize}
  \item any Coq type can be used as a datatype \par (shallow embedding)
  \item references and arrays of purely functional values
  \item sequences, conditionals, loops, local variables
  \item functions as first-class values, recursive functions
  \item call-by-value and call-by-reference
  \item restricted polymorphism
  \end{itemize}
  \vfill
\end{slide}

\begin{slide}{}
  \slidehead{Specifications}
  \begin{itemize}
  \item pre- and post-conditions \remph{anywhere}, written $\correct{P}{e}{Q}$
  \item loop invariants and variants
    $$\kw{while} ~ b ~ \kw{do} ~ \{ ~ [\kw{invariant} ~ I] ~
    \kw{variant} ~ \phi ~ [\kw{for} ~ R] ~ \} ~ e ~ \kw{done}$$
  \item variants for recursive functions
    $$\kw{let rec} ~ f ~ (\overrightarrow{x:T}) : T ~ \{ ~
    \kw{variant} ~ \phi ~ [\kw{for} ~ R] ~ \} ~ = e$$
  \item assertions (for convenience)
    $$\kw{begin} ~ e_1; \dots; \kw{assert} ~ \{ ~ P ~ \}; e_n; \dots ~
    \kw{end}$$
  \end{itemize}
  \vfill
\end{slide}

\begin{slide}{}
  \slidehead{Auxiliary variables}
  \dots are replaced by a notation for the successive values of a
  reference
  \begin{itemize}
  \item $x@$ stands for the value of $x$ \remph{before}
    $$\dots \correct{P}{e}{\dots x@\dots}\dots$$
  \item $x@0$ stands for the \remph{initial} value of $x$
  \item $x@L$ stands for the value of $x$ \remph{at label $L$}
    $$\dots; ~ \kw{label} ~ L; ~ \dots; ~ \dots \{ \dots x@L \dots \}
    ~ \dots$$
  \end{itemize}
  \vfill
\end{slide}

\begin{slide}{}
  \slidehead{Proof obligations}
  are the usual ones of Floyd-Hoare logic
  \begin{itemize}
  \item conditional $\Rightarrow$ two proof obligations, each one
    under the right hypothesis
  \item loop $\Rightarrow$ three proof obligations : initial
    invariant, preservation of invariant, termination
  \item etc.
  \end{itemize}
\end{slide}

\begin{slide}{}
  \slidehead{Expected context of hypotheses}
  \begin{displaymath}
    \begin{array}{l}
      \rouge \{ ~ (\id{Even} ~ n) ~ \} \\
      \kw{while} ~ !n > 0 ~ \kw{do} \\
      ~~ \rouge \{ ~ \kw{invariant} ~ (\id{Even} ~ n) ~ \kw{variant} ~ n ~ \} \\
      ~~ n ~ := ~ !n - 2; \\
      \kw{done} \\
      \rouge \{ ~ n = 0 ~ \}
    \end{array}
  \end{displaymath}
\end{slide}

\begin{slide}
  \slidehead{Arrays}
  Arrays are seen as references on a functional and abstract notion of array
  \begin{displaymath}
    \begin{array}{lcl}
      \kw{access} & : & (\kw{array} ~ N ~ T) \rightarrow Z \rightarrow
      T \\[-0.2em]
      \kw{store}  & : & (\kw{array} ~ N ~ T) \rightarrow Z \rightarrow
      T \rightarrow (\kw{array} ~ N ~ T)
    \end{array}
  \end{displaymath}
  %Obligations expressing correct accesses are automatically inserted
  %($0 \le i < N$)
  \begin{displaymath}
    \begin{array}{l}
      t_0 : (\kw{array} ~ N ~ T) \\[-0.4em]
      t_1 : (\kw{array} ~ N ~ T) \\
      \hline
      (\kw{access} ~ t_1 ~ i) < \underbrace{(\kw{access} ~ (\kw{store}
      ~ t_0 ~ i ~ v) ~ i)}_{reduced~to~v} 
    \end{array}
  \end{displaymath}
\end{slide}

%%%% 4. etudes de cas %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{slide}{}
  \slidehead{Case studies}
  \begin{itemize}
  \item Find (Hoare, 1971)
  \item Quicksort
  \item Heapsort
  \item Knuth-Pratt-Morris
  \item Binary Search
  \end{itemize}
\end{slide}

\begin{slide}{}
  \slidehead{Statistics}
  \hspace*{-0.7cm}
  \begin{tabular}{l|r|r|r|r|r}
                  & lines   & number & number & lines & total  \\[-0.6em]
                  & of code & annot. & oblig. & proof & time \\
    \hline\hline
    Find (Hoare, 71)   & 27 (1) &  9 & 22 & 619 & --- \\
    \hline
    Quicksort          & 41 (4) & 18 & 26 & 468 & 2 days \\
    \hline
    Heapsort           & 19 (2) &  7 & 22 & 626 & 3 days \\  
    \hline
    Knuth-Morris-Pratt & 24 (2) &  8 & 23 & 377 & 1,5 days \\
    \hline
    Binary Search      & 12 (1) &  3 &  8 & 146 & 3 hours \\
    \hline
  \end{tabular}
\end{slide}

\begin{slide}
  \slidehead{Proving programs...}
  \begin{itemize}
  \item is great fun!
  \item is not so hard (a few days for a complex algorithm)
  \item requires high mathematics, to specify and to prove
  \item automatic proofs seem hopeless
  \item the linear arithmetic decision procedure (Omega) was really useful
  \end{itemize}
\end{slide}

\begin{slide}{}
  \slidehead{Use of inductive predicates}
%   \vspace*{-0.5cm}
%   \begin{center}
%     \begin{tabular}{|l|c|r|r|}
%       \multicolumn{1}{l}{0} & \multicolumn{1}{c}{$k$} & 
%       \multicolumn{1}{r}{$n$} & \multicolumn{1}{r}{} \\
%       \hline
%       \hspace*{1.5cm} & & \hspace*{3cm} & \hspace*{2.5cm} \\
%       \hline
%     \end{tabular}
%   \end{center}
%   \medskip
  The $\mathit{heap}$ property is an \remph{inductive} predicate
\begin{displaymath}
  \irule
  {\begin{array}{c}
      2k+1 \le n \Rightarrow 
        (t[k] \ge t[2k+1] \land (\mathit{heap} ~ t ~ n ~ (2k+1))) \\[0.4em]
      2k+2 \le n \Rightarrow
        (t[k] \ge t[2k+2] \land (\mathit{heap} ~ t ~ n ~ (2k+2)))
   \end{array}}
  {(\mathit{heap} ~ t ~ n ~ k)}
\end{displaymath}
  Some proof obligations were established using the corresponding
  induction principle, and others using the induction principle
  {\small
  $P(0) ~\land~
   \forall n. ~ P(n) \Rightarrow P(2\cdot n+1) \land P(2\cdot n+2)
   \Rightarrow \forall n. ~ P(n)$}
\end{slide}

\begin{slide}{}
  \slidehead{Other case studies}
  \begin{itemize}
  \item Floyd's algorithm (all shortest paths in a weighted graph)
    (Christine Paulin)
  \item Petersson's mutual exclusion algorithm \par (Eduardo Giménez)
  \item Insertion sort (Nicolas Magaud)
  \item RSA (Jose-Carlos Almeida)
  \end{itemize}
\end{slide}

%%%% 5. Comparaisons %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{slide}{}
  \slidehead{Comparisons with other works}
  Shallow embeddings
  \begin{itemize}
  \item Hoare logic in HOL (M. Gordon, 96)
  \item B method in PVS (C. Mu\~noz, 98)
  \end{itemize}
  \vfill
  Deep embeddings
  \begin{itemize}
  \item Hoare logic in Lego (T. Kleymann, 97)
  \item B method in Isabelle/HOL (P. Chartier, 98)
  \item Hoare logic in HOL (P. Homeier, 96)
  \end{itemize}
\end{slide}

\begin{slide}{}
  \slidehead{Conclusion}
  We propose a method to certify imperative programs which
  \begin{itemize}
  \item combines a realistic programming language, a good
    specification language (CIC) and a good prover
  \item is implemented in Coq (distributed with the system)
  \item has been successfully applied to non-trivial case studies
  \end{itemize}
\end{slide}

\begin{slide}{}
  \slidehead{Future work}
  \begin{itemize}
  \item exceptions
  \item pattern-matching
  \item a purely functional case study \par
    (and to unify the tactics Program and Correctness)
  \end{itemize}
\end{slide}

\begin{slide}{}
  \slidehead{Availability}
  \begin{center}
    coq.inria.fr \\[1em]
    \red www.csl.sri.com/\unixtilde{}filliatr
  \end{center}

  \medskip
  \begin{itemize}
  \item a 40 pages english translation of my thesis
  \item a paper about generalized monads
  \item papers describings the case studies
  \end{itemize}
\end{slide}

\end{document}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: 
