%% Time-stamp: <modified on 13 Oct 2004 at 17:45 by Pierre Lescanne>
%% denotationnelle.tex
\documentclass[%
  slidesonly,%  Pour sortir les transparents seuls
%  semrot,%      Permettre des rotations eventuelles
  semhelv,%    Helvetica
  a4%           A4 paper
  ]{seminar}

\usepackage{fancybox}
\usepackage[francais]{babel}
\usepackage[latin1]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{color}
\usepackage{epsfig}
%\usepackage{stmaryrd,amssymb}
%\usepackage[dvips]{graphicx}
%\usepackage{amsmath}
\usepackage[all]{xy}
\usepackage{qsymbols}
\usepackage{prooftree}

%\def\printlandscape{\special{landscape}}    % pour sortir en landscape
                                            % avec dvips


\slidesmag{5}
\articlemag{1}


\title{\color{red}{\textit{Différentes sémantiques d'un langage impératif}}}

\author{}

\date{}

\newcommand{\logoLIP}{\includegraphics*[height=0.04\textwidth]{lipllipl.eps}}
\newcommand{\logoENS}{\includegraphics*[height=0.04\textwidth]{liplensl.eps}}
\newcommand{\logos}{\hspace*{12pt}Cours de sémantique --- automne 2004\hfill\logoENS }


\newpagestyle{AvecLogos}%
  {\hfil \thepage \rightmark}
{\logos}


\pagestyle{AvecLogos}

%\pagestyle{empty}

\slidestyle{empty}

\slideframe{}   


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                couleurs
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\input{mes_couleurs}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                symobles
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\ratwo}{\stackrel{\scriptscriptstyle 2}{\longrightarrow}}
\newcommand{\imp}{\rightarrow}
\newcommand{\rra}{\rouge{"->"}}
\newcommand{\rrastar}{\rouge{\rastar}}
\newcommand{\rratwo}{\rouge{\ratwo}}
\newcommand{\ali}{\newline\hspace*{20pt}}
\newcommand{\vdach}{\mathrel{\bl{\vdash}}}
\newcommand{\substit}[3]{#1[#2\leftarrow #3]}
\newcommand{\jdgv}[3]{\bleu{#1\vdash\verdir{#2}, #3}}
\newcommand{\jdge}[3]{\bleu{#1, \verdir{#2} \vdash #3}}
\newcommand{\jdg}[2]{\bleu{#1\vdash #2}}
\newcommand{\Jdgv}[3]{#1\vdash\verdir{#2}, #3}
\newcommand{\Jdge}[3]{#1, \verdir{#2} \vdash #3}
\newcommand{\Jdg}[2]{#1\vdash #2}
\newcommand{\und}[1]{\underline{#1}}
\newcommand{\x}{\ensuremath{\textbf{x}}}
\newcommand{\y}{\ensuremath{\textbf{y}}}
\newcommand{\lx}{\ensuremath{`l \texttt{x}}}
\newcommand{\lxgc}{\ensuremath{`l \texttt{x}_{gc}}}
\newcommand{\F}{\ensuremath{{\cal F}}}
\newcommand{\I}{\mathbf{I}}
\newcommand{\K}{\mathbf{K}}
\renewcommand{\S}{\mathbf{S}}
\newcommand{\llbda}{\mathbf{\lambda\hspace{-.58em}\lambda}}
\newcommand{\Nat}{\mathbb{N}}
\newcommand{\T}{\ensuremath{\mathbb{T}}}
\newcommand{\ifthenelse}[3]{\textbf{if~}#1\textbf{~then~}#2\textbf{~else~}#3}
\newcommand{\while}[2]{\textbf{while~}#1\textbf{~do~}#2}
\newcommand{\interp}[3]{\llbracket#1\rrbracket^{#2}_{#3}}
\newcommand{\Ainterp}[1]{\mathcal{A}\llbracket#1\rrbracket}
\newcommand{\Avinterp}[1]{\mathcal{A}v\llbracket#1\rrbracket}
\newcommand{\Binterp}[1]{\mathcal{B}\llbracket#1\rrbracket}
\newcommand{\Cinterp}[1]{\mathcal{C}\llbracket#1\rrbracket}
\newcommand{\modval}[3]{#1\rouge{(}#2\rouge{:=}#3\rouge{)}}
\newcommand{\prepost}[3]{\rouge{\{ #1\}}~#2~\rouge{\{#3\}}}
\renewcommand{\wp}[2]{wp^{`r}\llbracket#1, #2\rrbracket}
\newcommand{\set}[2]{\{#1~|~#2\}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%        les symboles pour les substitutions explicites
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% <...> are angle brackets.
\mathcode`\<=\string"4268 \mathcode`\>=\string"5269 %

\newcommand{\Lift}{\Uparrow\!\!}
\newcommand{\rabeta}{\rasub{\beta}}
\newcommand{\rarabeta}{\rarasub{\beta}}

%%%%%%%%%%%%%%%%%%%% fleches avec souscrit et superscrit %%%%%%%%%%%%%
% par exemple -- B, p --> s'ecrit \rasub{B,p}

\newcommand{\rasub}[1]{\xymatrix @C 15pt {\ar@{>}[r]_{#1} &}}
\newcommand{\ranormsub}[1]{\xymatrix @C 15pt {\ar@{>>|}[r]_{#1} &}}
\newcommand{\rarasub}[1]{\xymatrix @C 15pt {\ar@{>>}[r]_{#1} &}}
\newcommand{\rasup}[1]{\xymatrix @C 15pt {\ar@{>}[r]^{#1} &}}
\newcommand{\rarasup}[1]{\xymatrix @C 15pt {\ar@{>>}[r]^{#1} &}}
\newcommand{\rasupsub}[2]{\xymatrix @C 15pt {\ar@{>}[r]^{#1}_{#2} &}}
\newcommand{\conv}[1]{\xymatrix @C 25pt {\ar@{<<->>}[r]_{#1} &}}
\newcommand{\subar}[1]{\xymatrix @C 15pt {\ar@{<-}[r]_{#1} &}}

%%%%%%%%%%%%%%%%%%% -- B --> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\raB}{\rasub{B}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                environnements
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newenvironment{displaymathbleu}%
  {\begin{displaymath}\color{blue}}
  {\end{displaymath}}

\newenvironment{eqnarraybleu}%
  {\begin{color}{blue}\begin{eqnarray*}}
  {\end{eqnarray*}\end{color}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                headings
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\heading}[1]{%
{\color{cyanp}\bf\large #1}{\color{yellow}\\\rule{\textwidth}{2pt}}
}

\newcommand{\subheading}[1]{%
  \begin{center}
    \color{vertfonce}{\bf\Ovalbox{#1}}
  \end{center}}

 \newcount\timehh\newcount\timemm \timehh=\time 
 \divide\timehh by 60 \timemm=\time
 \count255=\timehh\multiply\count255 by -60 \advance\timemm by \count255

\newcommand{\timestamp}
 { {\protect\small\sl\today\ -- 
 \ifnum\timehh<10 0\fi\number\timehh\,:\,
   \ifnum\timemm<10 0\fi\number\timemm}}

\begin{document}

%------------------------------------------------------
\begin{slide}
    \maketitle
    \addtocounter{slide}{-1}
    \slidepagestyle{empty}

\vfill 

\hfill\textit{\footnotesize version du \timestamp}

\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large  \bf \color{vertfonce}{\textit{Présentation du langage}} }
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les constituants d'IMP}
\bleu{\textbf{IMP}} est associé aux ensembles suivants:
\begin{itemize}
\item les \emph{entiers} \bleu{\Nat} repérés par \bleu{n,m},
\item les \emph{emplacements} (en anglais «locations») \bleu{\textbf{Loc}},
  repérés par \bleu{X, Y},
\item les \emph{expressions arithmétiques}, \bleu{\textbf{Aexp}} repérées par
  \bleu{a, a_i},
\item les \emph{expressions booléennes}, \bleu{\textbf{Bexp}} repérées par
  \bleu{b, b_i},
\item les \emph{commandes} (ou \emph{instructions}), \bleu{\textbf{Com}} repérées par
  \bleu{c, c_j}.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La syntaxe d'IMP}
Les \emph{expressions arithmétiques} \bleu{\textbf{Aexp}}
\begin{eqnarraybleu}
  a &::=& n ~|~ X ~|~ a_0 + a_1 ~|~ a_0 - a_1 ~|~ a_0 `* a_1
\end{eqnarraybleu}
Les \emph{expressions booléennes} \bleu{\textbf{Bexp}}
\begin{eqnarraybleu}
  b &::=& \textbf{true} ~|~ \textbf{false} ~|~ a_0 = a_1 ~|~ a_0 ``<=
  a_1 ~|~ `!b  ~|~ b_0 \vee b_1 ~|~ b_0 \wedge b_1
\end{eqnarraybleu}
Les \emph{Commandes} \bleu{\textbf{Com}}
\begin{eqnarraybleu}
  c &::=& \textbf{skip} ~|~ X := a  ~|~ c_0;c_1  ~|~ \ifthenelse{b}{c_0}{c_1}  ~|~ \while{b}{c}
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large  \bf \color{vertfonce}{\textit{La sémantique opérationnelle}} }
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{L'ensemble des états}
L'ensemble \bleu{`S: \textbf{Loc} "->" \Nat} des \emph{états} associe un
nombre à un emplacement.

Si \bleu{`s: `S} alors \bleu{`s(X)} est le \emph{contenu} de l'emplacement
  \bleu{\textbf{Loc}} %
  \ali dans l'état \bleu{`s}.
  
  Une expression arithmétique \bleu{a} qui attend d'être évaluée dans
  l'état \bleu{`s} se note \bleu{<a, `s>}

La \emph{relation d'évaluation} entre paires associe un nombre à une paire.
Elle est notée \bleu{<a,`s> "->" n}.  

\begin{footnotesize}
  C'est une sémantique «grande étape»..
\end{footnotesize}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Évaluation des expressions entières}
\emph{Évaluation d'un nombre}
\begin{eqnarraybleu}
  <n,`s> & "->" & n
\end{eqnarraybleu}
\emph{Évaluation d'un emplacement}
\begin{eqnarraybleu}
  <X,`s> & "->" & `s(X)
\end{eqnarraybleu}
\emph{Évaluation d'une somme}
\begin{displaymathbleu}
  \prooftree %
  <a_1, `s> "->" n_1 \qquad <a_2, `s> "->" n_2
 \justifies  <a_1 + a_2, `s>  "->" n
 \using n \textrm{~est la somme de~} n_1 \textrm{~et de~} n_2
 \endprooftree
\end{displaymathbleu}
\hfill autrement dit \bleu{n=n_1+_\Nat n_2}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Évaluation des expressions entières}
\emph{Évaluation d'une soustraction}
\begin{displaymathbleu}
  \prooftree %
  <a_1, `s> "->" n_1 \qquad <a_2, `s> "->" n_2
 \justifies  <a_1 - a_2, `s>  "->" n
 \using n \textrm{~est la soustraction de~} n_1 \textrm{~et de~} n_2
 \endprooftree
\end{displaymathbleu}
\emph{Évaluation d'un produit}
\begin{displaymathbleu}
  \prooftree %
  <a_1, `s> "->" n_1 \qquad <a_2, `s> "->" n_2
 \justifies  <a_1 `* a_2, `s>  "->" n
 \using n \textrm{~est le produit de~} n_1 \textrm{~et de~} n_2
 \endprooftree
\end{displaymathbleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Évaluation des expressions booléennes}
\emph{Évaluation d'une valeur booléenne}
\begin{eqnarraybleu}
  <\textbf{true},`s> & "->" & \textbf{true}
\end{eqnarraybleu}
\centerline{$\vdots$}
\emph{Évaluation d'un test d'inégalité}
\begin{displaymathbleu}
  \prooftree %
  <a_1, `s> "->" n_1 \qquad <a_2, `s> "->" n_2 %
  \justifies <a_1 ``<= a_2, `s> "->" t %
\endprooftree
\end{displaymathbleu}
où \bleu{t} est \bleu{\textbf{true}} si \bleu{n_1} est plus petit que
\bleu{n_2} et \bleu{t} est \bleu{\textbf{false}} autrement.  
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Évaluation des expressions booléennes}
\emph{Évaluation d'une disjonction}
\begin{displaymathbleu}
  \prooftree %
  <b_1, `s> "->" t_1 \qquad <b_2, `s> "->" t_2
 \justifies  <b_1 \wedge b_2, `s>  "->" t
 \endprooftree
\end{displaymathbleu}
où \bleu{t} est \bleu{\textbf{true}} si \bleu{t_1`=\textbf{true}} et
\bleu{t_1`=\textbf{true}} et \bleu{t} est \bleu{\textbf{false}} %
\ali autrement dit \bleu{t = t_1 \wedge_{\mathbb{B}} t_2}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Évaluation des instructions}
On suppose qu'au début de l'évaluation d'un programme, on se trouve
dans l'\emph{état initial} \bleu{`s_0} qui tel que
\begin{eqnarraybleu}
  (`A X\in \textbf{Loc})~`s_0(X) &=& 0
\end{eqnarraybleu}
Comme on sait l'évaluation d'une commande à partir d'un certain état
peut \emph{se terminer} ou \emph{diverger}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Évaluation des instructions}
Nous allons définir une relation
\begin{eqnarraybleu}
  <c, `s> & "->" & `s'
\end{eqnarraybleu}
qui signifie que 
\begin{enumerate}
\item dans l'état \bleu{`s}, l'instruction \bleu{c} se termine et 
\item le couple \bleu{ <c, `s>} rejoint (s'évalue en) l'état \bleu{`s'}.
\end{enumerate}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Évaluation des instructions}
Par exemple, on s'imagine que
\begin{eqnarraybleu}
  <X:= X+1, `s> & "->" & `s'
\end{eqnarraybleu}
signifiera que \bleu{`s'} est l'état
\begin{itemize}
\item tel que \bleu{`s'(Y)} est \bleu{`s(Y)} pour \bleu{Y \neq X} 
\item et tel que \bleu{`s'(X)} vaut \bleu{`s(X)} augmenté de \bleu{1}.
\end{itemize}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La notation $`s[m/X]$}
Si \bleu{`s\in `S} est un état, \bleu{m\in\Nat} est un naturel et
\bleu{X\in \textbf{Loc}} est un emplacement, on écrit 
\begin{eqnarraybleu}
  `s[m/X](X) &=&  m \\
  `s[m/X](Y) &=& `s(Y) \qquad \textrm{si~} Y\neq X.
\end{eqnarraybleu}

Ainsi on pourra écrire
\begin{eqnarraybleu}
  <X:= X+1, `s> & "->" & `s[`s(X)+_\Nat 1/X]
\end{eqnarraybleu}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les règles pour les instructions simples}
\emph{Commande vide}
\begin{displaymathbleu}
  <\textbf{skip}, `s> "->" `s
\end{displaymathbleu}

\emph{Affectation}
\begin{displaymathbleu}
  \prooftree
  <a,`s> "->" m %
  \justifies <X:=a, `s> "->" `s[m/X]
  \endprooftree
\end{displaymathbleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les règles pour les instructions composées}
\emph{Composition séquentielle}
\begin{displaymathbleu}
  \prooftree%
  <c_0, `s> "->" `s''\qquad  <c_1, `s''> "->" `s'%
  \justifies <c_0; c_1, `s> "->" `s'
  \endprooftree%
\end{displaymathbleu}
\emph{Composition conditionnelle}
\begin{displaymathbleu}
  \prooftree
  <b,`s> "->" \textbf{true} \qquad <c_0, `s> "->" `s'
  \justifies  <\ifthenelse{b}{c_0}{c_1}, `s> "->" `s'
  \endprooftree
\end{displaymathbleu}
\begin{displaymathbleu}
  \prooftree
  <b,`s> "->" \textbf{false} \qquad <c_1, `s> "->" `s'
  \justifies  <\ifthenelse{b}{c_0}{c_1}, `s> "->" `s'
  \endprooftree
\end{displaymathbleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les règles pour les instructions composées}
\emph{Boucles while}
\begin{displaymathbleu}
  \prooftree%
 <b,`s> "->" \textbf{false}
  \justifies <\while{b}{c}, `s> "->" `s
  \endprooftree%
\end{displaymathbleu}
\begin{displaymathbleu}
  \prooftree%
 <b,`s> "->" \textbf{true} \qquad <c, `s>  "->" `s'' \qquad <\while{b}{c}, `s''> "->" `s'
  \justifies <\while{b}{c}, `s> "->" `s'
  \endprooftree%
\end{displaymathbleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les règles pour les instructions composées}
\emph{Boucles while}
\begin{displaymathbleu}
  \prooftree%
 <b,`s> "->" \textbf{false}
  \justifies <\while{b}{c}, `s> "->" `s
  \endprooftree%
\end{displaymathbleu}
\begin{displaymathbleu}
  \prooftree%
 <b,`s> "->" \textbf{true} \qquad <c, `s>  "->" `s'' \qquad <\while{b}{c}, `s''> "->" `s'
  \justifies <\while{b}{c}, `s> "->" `s'
  \endprooftree%
\end{displaymathbleu}


Noter que la définition ne se fait pas par induction sur la longueur
de la commande.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large  \bf \color{vertfonce}{\textit{Une sémantique «petite étapes»\\
          des expressions }} }
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Une alternative}
%
On veut être plus proche de l'évaluation des expressions.

La relation se fait entre paires \emph{expression--état} du type
\begin{eqnarraybleu}
  <a,`s> & "(pe)>" & <a',`s'>
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Une alternative}
%
On aurait alors
\begin{displaymathbleu}
  \prooftree
  <a_0, `s> "(pe)>" <a_0', `s> %
  \justifies <a_0 + a_1 , `s> "(pe)>" <a_0' + a_1, `s> %
  \endprooftree
\end{displaymathbleu}
\begin{displaymathbleu}
  \prooftree
  <a_1, `s> "(pe)>" <a_1', `s> %
  \justifies <n + a_1 , `s> "(pe)>" <n + a_1', `s> %
  \endprooftree
\end{displaymathbleu}
\begin{displaymathbleu}
  <n + m , `s> "(pe)>" <n +_\Nat m, `s> %
\end{displaymathbleu}
Cela formalise une évaluation de gauche à droite des expressions.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large  \bf \color{vertfonce}{\textit{Points fixes, fonctionnelles et récursivité }} }
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La fonction de McCarthy}
Considérons la définition 
\begin{eqnarraybleu}
\textrm{let rec~}m~x & = &   \ifthenelse{x ``> 100}{x-10}{m~(m~(x+11))}
\end{eqnarraybleu}
A priori cela définit une \emph{fonction partielle} (sauf pour les valeurs de
\bleu{x``>100} pour lesquelles on est certain de la valeur).

\vspace*{20pt}

Laquelle ?

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Un ordre sur les fonctions}%
%
Nous dirons que \bleu{h ``[= g} si \bleu{h} est \emph{moins définie}
que \bleu{g}\footnote{si \bleu{h} est définie en \bleu{x}, alors
  \bleu{g} est aussi définie en \bleu{x}}\\
 et là où \bleu{h} et
\bleu{g} sont définies ensembles elles prennent la même valeur.

Un \emph{dirigé} \bleu{F} dans \bleu{(\Nat "^->" \Nat)} est un
ensemble de fonctions partielles tel que s'il contient deux fonctions
\bleu{h} et \bleu{g} il contient
\begin{itemize}
\item une fonction \bleu{l} encore plus définie que chacune d'elles,\\
\qquad c'est-à-dire si \bleu{h(x)} ou  \bleu{g(x)} est défini, alors \bleu{l(x)} est défini,
\item et telle que \bleu{l}  coïncide avec chacune d'elles sur leurs
  domaines de définition.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Un ordre sur les fonctions}%
%
Un \emph{majorant} de \bleu{E} est un élément \bleu{m} tel que \bleu{(`A x`:
  E)\ x ``[= m.}.

La \emph{borne supérieure} est le plus petit des majorants.
\vfill
Une fonction est \emph{continue} si elle préserve les bornes
supérieures.
\begin{displaymathbleu}
  f(\sup E) = \sup f(E).
\end{displaymathbleu}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Fonction continue et point fixe}%
On note tout d'abord que si un ensemble est tel que que toute partie a
une borne supérieure,

alors il a un plus petit élément qui est la borne supérieure \bleu{\bot} de
l'ensemble vide.

On peut montrer que toute fonction continue admet une point fixe:
\begin{displaymathbleu}
  \sup\set{f^n(\bot)}{n\in \Nat}.
\end{displaymathbleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Fonctionnelles et points fixes}
Considérons la \emph{fonctionnelle} \bleu{F}
\begin{eqnarraybleu}
  F(g) & = & \llbda x . \ifthenelse{x ``> 100}{x-10}{g~(g~(x+11))}.
\end{eqnarraybleu}
La fonctionnelle \bleu{F} est \emph{continue}.  En effet,
\begin{itemize}
\item \bleu{\llbda g . \llbda x .  g~(g~(x+11))} est continue par rapport
  à  \bleu{g}.
\item \bleu{\llbda g . \llbda x .  \ifthenelse{b(x)}{G(g)(x)}{H(g)(x)}}
    est continue par rapport à \bleu{g} si \bleu{G} et \bleu{H} sont
    continues.
\end{itemize}

\bleu{F} a donc un point fixe \bleu{Fix(F)} tel que \bleu{F(Fix(F)) =
  Fix(F)}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Fonctionnelles et points fixes}
Le point fixe de \bleu{F} est obtenu en itérant \bleu{F} à partir de
la fonction \bleu{\bot} nulle part définie.
\begin{eqnarraybleu}
  F(\bot) (x) & = & \textbf{if~}{x ``> 100} \textbf{~then~} {x-10}\\
   F^2(\bot) (x) & = & \ifthenelse{x ``> 100}{x-10}{F(\bot)~(F(\bot)~(x+11))}\\
   &\vdots &\\
  F^{n+1}(\bot) (x) & = & \ifthenelse{x ``> 100}{x-10}{F^n(\bot)~(F^n(\bot)~(x+11))}\\
   &\vdots &
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Fonctionnelles et points fixes}
\begin{displaymathbleu}
  Fix(F) = \sup_{n\in\Nat} F^n(\bot)
\end{displaymathbleu}

Comme \bleu{F} est continue on 
  \begin{displaymathbleu}
    F(Fix(F)) = Fix(F)
  \end{displaymathbleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Le points fixe de \bleu{F}}
\bleu{Fix(F)} est la fonction \bleu{m} définie par
\begin{eqnarraybleu}
\textrm{let rec~}m~x & = &   \ifthenelse{x ``> 100}{x-10}{m~(m~(x+11))}
\end{eqnarraybleu}
C'est aussi la fonction
\begin{eqnarraybleu}
\textrm{let rec~}m~x & = &   \ifthenelse{x ``> 100}{x-10}{91}
\end{eqnarraybleu}

\begin{enumerate}
\item Encore faudrait-il le prouver !
\item En sémantique dénotationnelle on s'intéresse aux
  fonctions~\footnote{Même si nous intéressons aux fonctions
    calculables plutôt qu'aux algorithmes !}  \emph{dénotée} par le
  programme.
\end{enumerate}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large  \bf \color{vertfonce}{\textit{Une sémantique dénotationnelle
          de IMP }} }
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Quelques remarques}
%
La sémantique opérationnelle \emph{mélange} la syntaxe et les états dans sa définition.

Elle \emph{colle} de très (trop) \emph{près} à la syntaxe.

Et encore pas de la meilleure manière puisque la définition ne fait \emph{pas
par induction sur la syntaxe}.

Ce qu'on cherche à définir c'est une \emph{fonction} (au sens mathématique du
terme).

On pourra de cette manière considérer des \emph{programmes} qui sont
\emph{équivalents} parce qu'ils définissent \emph{la même fonction mathématique}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les fonctions de base}

\bleu{\Ainterp{a}:  `S  "->" \Nat},

\bleu{\Binterp{b}: `S   "->" \T},

\bleu{\Cinterp{c}: `S "^->" `S} %

\hfill \bleu{`S "^->"`S } représente l'ensemble des fonctions partielles de
\bleu{`S} vers \bleu{`S}.

On a donc les fonctions d'interprétation sémantique

\bleu{\Ainterp{\quad}: \textbf{Aexp} "->"  `S  "->" \Nat},

\bleu{\Binterp{\quad}: \textbf{Bexp} "->"  `S  "->" \T},

\bleu{\Cinterp{\quad}: \textbf{Com} "->"`S "^->" `S}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La dénotation des \textbf{Aexp}}
\begin{eqnarraybleu}
  \Ainterp{n} `s & = & n\\
  \Ainterp{X} `s & = & `s(X)\\
  \Ainterp{a_0 + a_1} `s & = & \Ainterp{a_0} `s +_\Nat \Ainterp{a_1} `s \\
\Ainterp{a_0 - a_1} `s & = & \Ainterp{a_0} `s -_\Nat \Ainterp{a_1} `s \\
\Ainterp{a_0 `* a_1} `s & = & \Ainterp{a_0} `s `*_\Nat \Ainterp{a_1} `s \\
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La dénotation des \textbf{Aexp}}
\begin{eqnarraybleu}
  \Ainterp{n}  & = &  \llbda `s . n\\
  \Ainterp{X}  & = & \llbda `s . `s(X)\\
  \Ainterp{a_0 + a_1}  & = & \llbda `s . (\Ainterp{a_0} `s +_\Nat \Ainterp{a_1} `s) \\
  \Ainterp{a_0 - a_1}  & = & \llbda `s . (\Ainterp{a_0} `s -_\Nat \Ainterp{a_1} `s) \\
  \Ainterp{a_0 `* a_1}  & = & \llbda `s . (\Ainterp{a_0} `s `*_\Nat \Ainterp{a_1} `s) \\
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La dénotation des \textbf{Bexp}}
\begin{eqnarraybleu}
  \Binterp{\textbf{true}}  & = &  \llbda `s . \textbf{true}\\
  \Binterp{\textbf{false}}  & = &  \llbda `s . \textbf{false}\\
  \Binterp{a_0 = a_1}  & = & \llbda `s . (\Ainterp{a_0}`s  =_\Nat  \Ainterp{a_1} `s) \\
      & \vdots & \\
  \Binterp{b_0 \wedge b_1}  & = & \llbda `s . (\Binterp{b_0}`s
  \wedge_\T \Binterp{b_1} `s) \\
      & \vdots & 
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La dénotation des instructions}
\begin{eqnarraybleu}
           \Cinterp{\textbf{skip}} & = & \llbda `s . `s \\
  \Cinterp{X:=a} & = & \llbda `s . `s[X/\Ainterp{a}`s]\\
  \Cinterp{c_0; c_1} & = & \Cinterp{c_1} `o \Cinterp{c_0}
\end{eqnarraybleu}
\begin{eqnarraybleu}
  \Cinterp{\ifthenelse{b}{c_0}{c_1}}`s & = & \Cinterp{c_0}`s \qquad
  \texttt{si~} \Binterp{b}`s \\
  \Cinterp{\ifthenelse{b}{c_0}{c_1}}`s & = & \Cinterp{c_1}`s \qquad
  \texttt{si~} \neg \Binterp{b}`s
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La dénotation de la boucle while}
On cherche à dénoter la commande  \bleu{\while{b}{c}}.

Soit \bleu{g\in `S "^->" `S}.

Considérons la «fonctionnelle» \bleu{`G_g : (`S "^->" `S) "->"  (`S "^->" `S)}.
\begin{eqnarraybleu}
  `G_g(f)`s & = & (f `o g) `s \qquad
      \texttt{si~} \Binterp{b}`s \\
   `G_g(f)`s & = & `s  \qquad \quad \texttt{si~} \neg \Binterp{b}`s 
\end{eqnarraybleu}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{La fonctionnelle \bleu{`G_g}}%
%
La fonctionnelle \bleu{`G_g} est continue pour la relation \bleu{``[=}.
\begin{eqnarraybleu}
  (\sup_{h\in F} `G_g(h))`s &= & ((\sup_{h\in F} h) `o g) `s  \qquad
      \texttt{si~} \Binterp{b}`s \\
  (\sup_{h\in F} `G_g(h))`s & = & `s \qquad \quad \texttt{si~} \neg \Binterp{b}`s 
\end{eqnarraybleu}

La fonctionnelle \bleu{`G_g} a un point fixe \bleu{Fix(`G_g)} \ali qui est une
fonction partielle de \bleu{`S} vers \bleu{`S}.
\begin{eqnarraybleu}
  Fix(`G_g) &:& `S "^->" `S.
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La dénotation de la boucle while}
%
Remarquons que \bleu{`G_g(\bot)} n'est défini que sur les états
\bleu{`s} tels que \bleu{\neg\Binterp{b}`s} et qu'alors 
\begin{eqnarraybleu}
  `G_g(\bot)`s & = & `s
\end{eqnarraybleu}
et que \bleu{`G_g^{n+1}(\bot)} est défini sur les états \bleu{`s} tels
que 
\begin{itemize}
\item \bleu{g^{i}`s} est défini pour \bleu{i``<= n+ 1} 
\item et \bleu{\Binterp{b} g^{i}`s} pour \bleu{i``<= n}, tandis que
  \bleu{\neg \Binterp{b} g^{n+1}`s}.
\end{itemize}
Et on a 
\begin{eqnarraybleu}
  `G_g^{n+1}(\bot)(`s) &=& g^{n+1}(`s).
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La dénotation de la boucle while}
%
Le point fixe de \bleu{`G_g} est donc défini pour tous les \bleu{`s}
tels qu'il existe un~\bleu{n} avec 
\begin{itemize}
\item \bleu{g^i(`s)} défini et
  \bleu{\Binterp{b} g^i(`s)} pour \bleu{i``< n} 
\item et \bleu{g^n(`s)}
  défini et \bleu{\neg \Binterp{b} g^n(`s)}.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La dénotation de la boucle while}
%
En fait, on s'intéresse à la fonctionnelle
\begin{eqnarraybleu}
  `G_{\Cinterp{c}}(f)`s & = & (f `o \Cinterp{c}) `s \qquad
      \texttt{si~} \Binterp{b}`s \\
   `G_{\Cinterp{c}}(f)`s & = & `s  \qquad \quad \texttt{si~} \neg \Binterp{b}`s 
\end{eqnarraybleu}


On pose
\begin{eqnarraybleu}
  \Cinterp{\while{b}{c}} & = & Fix(`G_{\Cinterp{c}}).
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{vertfonce}{\textit{Une sémantique axiomatique de
          IMP }} }
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Qu'est-ce que l'annotation d'un programme par des
    assertions ?}%
%
  A départ, il s'agit de prouver la correction des programmes en
  examinant des \emph{instantanés}~\footnote{L'expression
    \emph{snapshot} et due à Floyd.} successifs de l'état pendant le
  déroulement du programme.
  
  Les concepteurs voulaient seulement prouver des propriétés des
  programmes.

Aujourd'hui c'est utilisé \textit{aussi} pour décrire leur signification.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{La notation des assertions}%
%
On va énoncer  des \emph{assertions de corrections} sur
des instructions.

Puis des des règles d'inférence sur ces assertions de correction.

Les assertions de corrections s'écriront
                                % \prepost{A}{c}{B}  est une notation
                                % pour quelque chose qui s'écrirait
                                % simplement {A}c{B} .
\begin{displaymathbleu}
  \prepost{A}{c}{B}
\end{displaymathbleu}
\emph{A} est la \emph{précondition} de \bleu{c}.

\emph{B} est la \emph{postcondition de correction partielle} de
\bleu{c}.

L'assertion doit se lire 
\begin{quotation}
  «Si \emph{A} est satisfaite avant l'exécution de \bleu{c} et si
  l'exécution de \bleu{c} \emph{se termine} alors \emph{B} est satisfaite
  après l'exécution de \bleu{c}».
\end{quotation}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{L'annotation d'un programme}%
%
  Si l'on veut annoter un programme par des propriétés, on utilise une
  notation comme celle-ci

\emph{Pre}: \bleu{Condition_1}
\begin{verbatim}
Texte
...
    du
...
programme
\end{verbatim}
\emph{Post:} \bleu{Condition_2}

C'est très commode pour la mise au point.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{L'annotation d'un programme}%
%
\emph{Pre}: \bleu{Condition_1}
\begin{verbatim}
Texte
...
    du
...
programme
\end{verbatim}
\emph{Post:} \bleu{Condition_2}

est équivalent à %
\bleu{\prepost{Condition_1}{\texttt{Texte ... du ... programme}}{Condition_2}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Un exemple}%
Considérons
\begin{verbatim}
q := 0;
r := x;
while r >= y do
    {r := r - y;
    q := q +1}
\end{verbatim}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Un exemple}%
On annote le programme

\emph{Pre}: \bleu{x ``>= 0}
\begin{verbatim}
q := 0;
r := x;
while r >= y do
    {r := r - y;
    q := q +1}
\end{verbatim}
\emph{Post:} \bleu{0 ``=< r ``< y \quad \wedge \quad x = q `* y + r}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Pre Post}%
\emph{Pre} représente l'instantané avant l'exécution du programme.

\emph{Post} représente l'instantané après.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Un exemple}%
Compte tenu de ce qu'on a dit, on a aussi

\emph{Pre}: \bleu{x ``>= 0}
\begin{verbatim}
q := 0;
r := x;
while r >= y do
    {r := r + y;
    q := q +1}
\end{verbatim}
\emph{Post:} \bleu{0 ``=< r ``< y \quad \wedge \quad x = q `* y + r}

Car comme la boucle ne va jamais s'arrêter, la définition est satisfaite.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Collection de quelques propriétés}%
  Puisque la condition d'exécution de la boucle est \bleu{r ``>= y} %
  \ali après la boucle on a \bleu{\neg (r ``>= y)} donc \bleu{r ``< y}.

Comme on exécute la boucle sous la condition \bleu{r ``>= y},
la soustraction \bleu{r - y} produira toujours une valeur positive et
\bleu{r} sera toujours positif~\footnote{A condition que ?}.

On introduit donc naturellement la notion d'\emph{invariant} de
boucle, c'est-à-dire une propriété qui \verdir{reste satisfaite} du début à la
fin de l'exécution de la boucle.

\begin{itemize}
\item \bleu{r ``>= 0} est un invariant de la boucle.
  
\item \bleu{ x = q `* y + r} est un autre invariant.
\end{itemize}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les deux premières instructions}%
%
\emph{Pre}: \bleu{x ``>= 0}
\begin{verbatim}
q := 0;
r := x;
\end{verbatim}
\emph{Post}: \bleu{x ``>= 0 \quad \wedge \quad q = 0 \quad \wedge
  \quad r = x}


\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les deux premières instructions}%
%
\emph{Pre}: \bleu{x ``>= 0}
\begin{verbatim}
q := 0;
r := x;
\end{verbatim}
\emph{Post}: \bleu{x ``>= 0 \quad \wedge \quad q = 0 \quad \wedge
  \quad r = x}

Duquel on déduit qu'après ces deux instructions on a 
\begin{displaymathbleu}
  r ``>= 0 \quad \wedge \quad x = q `* y + r
\end{displaymathbleu}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Le corps de la boucle}%
%
On souhaite

\emph{Pre}: \bleu{r ``>= 0 \quad \wedge \quad x = q `* y + r}
\begin{verbatim}
r := r - y;
q := q +1
\end{verbatim}
\emph{Post}: \bleu{r ``>= 0 \quad \wedge \quad x = q `* y + r}

car c'est l'\emph{invariant} de la boucle.

Ça ne suffit pas.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Le corps de la boucle}%
%
Il faut

\emph{Pre}: \bleu{r ``>= y \quad \wedge \quad r ``>= 0 \quad \wedge \quad x = q `* y + r}
\begin{verbatim}
r := r - y;
q := q +1
\end{verbatim}
\emph{Post}: \bleu{r ``>= 0 \quad \wedge \quad x = q `* y + r}

Mais en fait \bleu{r ``>= y} est la \emph{condition} de la boucle, %
\ali donc elle est satisfaite, comme précondition.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les boucles}%
%
La règle concernant les boucles peut s'énoncer ainsi

\begin{quotation}
  On rentre dans le corps avec  \emph{Pre :} \bleu{b \quad \wedge
    \quad I}.
  
  On sort de toute la boucle~\footnote{Si toutefois on en sort !} avec
  \emph{Post :} \bleu{\neg b \quad \wedge \quad I}.
\end{quotation}
où \bleu{b} est la condition de la boucle

et \bleu{I} est l'invariant de la boucle
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les boucles}%
%
Plus formellement on écrit
\begin{displaymathbleu}
  \prooftree %
  \prepost{b \wedge I}{c}{I}
  \justifies \prepost{I}{\while{b}{c}}{\neg b \wedge I}
  \endprooftree
\end{displaymathbleu}

et l'on espère avoir tout dit!
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les boucles}%
%

\begin{displaymathbleu}
  \prooftree %
  \prepost{b \wedge I}{c}{I}
  \justifies \prepost{I}{\while{b}{c}}{\neg b \wedge I}
  \endprooftree
\end{displaymathbleu}

dit que
\begin{itemize}
\item si \emph{I} est satisfaite avant l'exécution de la boucle
\item et si la boucle se termine
 \end{itemize}
 alors $\rouge{\neg b \wedge I}$ est satisfaite.%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les affectations}%
%
On a

\emph{Pre}: ?
\begin{verbatim}
q := q +1
\end{verbatim}
\emph{Post}: \bleu{r ``>= 0 \quad \wedge \quad x = q `* y + r}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les affectations}%
%
En fait 

\emph{Pre}:  \bleu{r ``>= 0 \quad \wedge \quad x = (q+1) `* y + r}
\begin{verbatim}
q := q +1
\end{verbatim}
\emph{Post}: \bleu{r ``>= 0 \quad \wedge \quad x = q `* y + r}

Et

\vfill    \addtocounter{slide}{-1}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les affectations}%
%
\emph{Pre}:  \bleu{r -y``>= 0 \quad \wedge \quad x = (q+1) `* y + r - y}
\begin{verbatim}
r := r - y
\end{verbatim}
\emph{Post}: \bleu{r ``>= 0 \quad \wedge \quad x = (q + 1) `* y + r}

\centerline{{\color{green}\rule{100pt}{1pt}}}

\emph{Pre}:  \bleu{r ``>= 0 \quad \wedge \quad x = (q+1) `* y + r}
\begin{verbatim}
q := q +1
\end{verbatim}
\emph{Post}: \bleu{r ``>= 0 \quad \wedge \quad x = q `* y + r}

ce qui est bien ce qu'on veut parce que \bleu{(q+1) `* y + r - y = q
  `* y + r} et \bleu{r-y``>= 0 "<=>" r``>= y}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les affectations}%
%
La règle de l'affectation est donc
\begin{displaymathbleu}
  \prepost{\substit{B}{X}{a}}{X:=a}{B}
\end{displaymathbleu}

\vspace*{20pt}

Remarquer l'intérêt d'aller «en marche arrière» %
\ali plutôt qu'«en marche avant».
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La signification d'une assertion de correction}%
%
\bleu{`s "|=" A} signifie que \bleu{A} est satisfaite dans l'état
\bleu{`s}.

\bleu{\prepost{A}{c}{B}} signifie
\begin{displaymathbleu}
  `A `s: `S . (`s  "|=" A \quad \& \quad \Cinterp{c}`s \textrm{~est défini}) "=>"
  \Cinterp{c}`s "|=" B
\end{displaymathbleu}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La signification d'une assertion de correction}%
%
En fait au lieu de \emph{est défini} on étend \bleu{\Cinterp{c}} en
une fonction totale qui vaut \bleu{\bot} là où \bleu{\Cinterp{c}} devrait ne pas
être définie et l'on pose
\begin{displaymathbleu}
  \bot "|=" A 
\end{displaymathbleu}
pour toute assertion \bleu{A}.

Avec cette convention on peut dire que \bleu{\prepost{A}{c}{B}} signifie
\begin{displaymathbleu}
  `A `s: `S . \quad `s  "|=" A"=>" \Cinterp{c}`s "|=" B
\end{displaymathbleu}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Le langage d'assertions}%
%
Pour pouvoir affirmer des propriétés de l'état, \\
il nous faut \emph{un langage assez riche.}

On veut
\begin{itemize}
\item tous les prédicats booléens du langage IMP,
\item des quantifications sur des valeurs entières,
\item ce qui induit qu'il faut introduire des variables libres
  destinées à être quantifiées.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Le langage enrichi des expressions \bl{\textbf{Aexpv}}}%
%
On définit tout d'abord le langage enrichi de \emph{variables libres} \bl{\textbf{Aexpv}}:
\begin{eqnarraybleu}
  a &::=& n ~|~ X ~|~ i ~|~ a_0 + a_1 ~|~ a_0 - a_1 ~|~ a_0 `* a_1
\end{eqnarraybleu}
où \bleu{i} sont des variables entières formant
\bleu{\textbf{Intvar}}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Le langage enrichi d'assertions \bl{\textbf{Bexpv}}}%
%
Les assertions portent sur ces expressions arithmétiques enrichies et
on y ajoute des implications et des quantifications sur les variables
de \bleu{\textbf{Intvar}}.

On définit \bl{\textbf{Bexpv}}:
\begin{eqnarraybleu}
  A &::=& \textbf{true} ~|~ \textbf{false} ~|~ a_0 = a_1 ~|~ a_0 ``<=
  a_1 ~|~ `!A  ~|~ A_0 \vee A_1 ~|~ A_0 \wedge A_1 \\
  && ~|~ A_0 "=>" A_1  ~|~ `A i. A  ~|~ `E i. A 
\end{eqnarraybleu}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Le langage d'assertions: substitutions}%
%
On peut faire des substitutions dans le langage d'assertions.

On les note \bleu{\substit{A}{i}{a}}.

\vspace*{20pt}

Une  \emph{valuation} est une fonction \bleu{`r: \textbf{Intvar }"->"
  \Nat}.


\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Sémantique des expressions arithmétiques enrichies}
%
On définit une fonction %
\bleu{\Avinterp{~} : \textbf{Aexpv} "->" (\textbf{Intvar}"->"  \Nat)
  "->" `S "->" `S}: 
\begin{eqnarraybleu}
  \Avinterp{n}`r `s &=& n\\
  \Avinterp{X}`r `s &=& `s(X)\\
  \Avinterp{i}`r `s &=&  `r(i)\\
  \Avinterp{a_0 +  a_1}`r `s &=& \Avinterp{a_0}`r `s +_\Nat  \Avinterp{a_1}`r `s\\
  \Avinterp{a_0 -  a_1}`r `s &=& \Avinterp{a_0}`r `s -_\Nat  \Avinterp{a_1}`r `s\\
  \Avinterp{a_0 `*  a_1}`r `s &=& \Avinterp{a_0}`r `s `*_\Nat  \Avinterp{a_1}`r `s
\end{eqnarraybleu}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Sémantique des assertions}
\subheading{La sémantique des expressions booléennes}
\begin{displaymathbleu}
  \begin{array}[c]{l@{"|="^{`r}}l@{\hspace*{30pt}\textrm{if~}}l} 
% j'utilise ce type tableau pour ne  pas répéter "|="^{`r}
        `s & \textbf{true} & \textit{rien}\\
        `s & a_0 = a_1 & \Avinterp{a_0}`r `s =_\Nat  \Avinterp{a_1}`r `s\\
        `s & a_0 ``<= a_1 & \Avinterp{a_0}`r `s ``<=_\Nat  \Avinterp{a_1}`r `s\\
        `s & A \wedge B & `s "|="^{`r} A \textrm{~et~} `s "|="^{`r} B \\
        `s & A \vee B & `s "|="^{`r} A \textrm{~ou~} `s "|="^{`r} B \\
        `s & \neg A & `s "|/="^{`r} A \\
  \end{array}
\end{displaymathbleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Sémantique des assertions}
\subheading{La sémantique des expressions booléennes}
\begin{displaymathbleu}
  \begin{array}[c]{l@{"|="^{`r}}l@{\hspace*{30pt}\textrm{if~}}l} 
    `s & A "=>" B & \textrm{de~} `s "|="^{`r} A \textrm{~on peut déduire~} `s "|="^{`r} B  \\
    `s & ~ `A i .  A & `s "|="^{\modval{`r}{i}{n}} A \textrm{~pour tout ~} n\in \Nat\\
   `s & ~ `E i .  A & `s "|="^{\modval{`r}{i}{n}} A \textrm{~pour un ~} n\in \Nat\\
   \bot & A & \textit{rien}  
  \end{array}
\end{displaymathbleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Quelques résultats}
On peut prouver que pour n'importe quelle valuation \bleu{`r}
\begin{itemize}
\item \bleu{\Binterp{b}`s = \textbf{true}} si et seulement si \bleu{`s "|="^{`r} b}
\item \bleu{\Binterp{b}`s = \textbf{false}} si et seulement si \bleu{`s "|/="^{`r} b}

\item \bleu{\Avinterp{a} \modval{`r}{i}{n} `s = \Avinterp{\substit{a}{i}{n}}`r`s}
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Satisfaction d'une assertion de correction}
\begin{center}
  \bleu{  "|="^{`r} \prepost{A}{c}{B}} \quad iff \quad \bleu{ `A `s: `S . `s  "|="^{`r}  A"=>" \Cinterp{c}`s "|="^{`r}  B}
\end{center}


\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Validité d'une assertion de correction}
\begin{center}
  \bleu{ "|=" \prepost{A}{c}{B}} \quad iff \quad pour
  toute valuation \bleu{`r} et tout état~\bleu{`s} \bleu{`s "|="^{`r}
    \prepost{A}{c}{B}}
\end{center}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
\heading{Les règles de correction partielle 1/4}
\brunir{Règle de l'instruction vide}:
\begin{displaymathbleu}
  \prepost{A}{\textbf{skip}}{A}
\end{displaymathbleu}
\brunir{Règle de l'affectation}:
%
\begin{displaymathbleu}
  \prepost{\substit{B}{X}{a}}{X:=a}{B}
\end{displaymathbleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
\heading{Les règles de correction partielle 2/4}
\brunir{Règle de la composition séquentielle}
\begin{displaymathbleu}
  \prooftree 
  \prepost{A}{c_0}{C} \quad \prepost{C}{c_1}{B}
  \justifies \prepost{A}{c_0;c_1}{B}
  \endprooftree
\end{displaymathbleu}
\brunir{Règle de la composition conditionnelle}:
%
\begin{displaymathbleu}
  \prooftree
  \prepost{A \wedge b}{c_0}{C} \quad \prepost{\neg b \wedge C}{c_1}{B}%
  \justifies \prepost{A}{\ifthenelse{b}{c_0}{c_1}}{B}
  \endprooftree
\end{displaymathbleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les règles de correction partielle 3/4}
%
\brunir{Règle de la boucle}:
%
\begin{displaymathbleu}
  \prooftree %
  \prepost{b \wedge I}{c}{I}
  \justifies \prepost{I}{\while{b}{c}}{\neg b \wedge I}
  \endprooftree
\end{displaymathbleu}

\brunir{Règle de conséquence}:

\begin{displaymathbleu}
  \prooftree %
  "|=" A "=>" A' \quad  \prepost{A'}{c}{B'} \quad "|=" B' "=>" B
  \justifies \prepost{A}{c}{B}
  \endprooftree
\end{displaymathbleu}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les règles de correction partielle 4/4}
%
Remarquer que la règle de conséquence s'appuie sur des propriétés «valides».
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{L'exemple}
Remarquons que l'on utilise la règle de conséquence, car
\vspace*{20pt}

\begin{tiny}
\begin{displaymathbleu}
\prooftree
  \parbox{9cm}{\bleu{
  "|=" r``>= y ~ \wedge ~ r ``>= 0 ~ \wedge ~ x = q `* y + r %
  \quad "=>" \quad  r - y``>= 0 ~ \wedge ~ x = (q+1) `* y + r - y} \\[3pt]
    \bleu{\prepost{r- y``>= 0 ~  \wedge ~ x = (q+1) `* y + r
      - y}{r := r - y; q := q +1}{r ``>= 0 ~ \wedge ~ x = q `* y + r}}\\[3pt] 
    \bleu{"|=" r ``>= 0 ~ \wedge ~ x = q `* y + r \quad "=>" \quad r
      ``>= 0 ~ \wedge ~ x = q `* y + r}\\~} %
    \justifies \prepost{r``>= y ~ \wedge ~
  r ``>= 0 ~ \wedge ~ x = q `* y + r}{r := r - y; q := q +1}{r ``>= 0
  ~ \wedge ~ x = q `* y + r} %
  \endprooftree
\end{displaymathbleu}
\end{tiny}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{vertfonce}{\textit{Correction de la sémantique
          axiomatique }} }
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Correction (cas des expressions arithmétiques)}%
\verdir{Lemme :} Soient \bleu{`r} une valuation, \bleu{a\in\textbf{Aexpv}},
\bleu{a_0\in\textbf{Aexpv}}, \bleu{X\in \textbf{Loc}}, \bleu{`s\in`S}
\begin{eqnarraybleu}
  \Avinterp{a_0[a/X]} `r `s &=&  \Avinterp{a_0} `r (`s[\Avinterp{a} `r `s/X])
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Correction (cas des expressions booléennes)}%
\verdir{Lemme :} Soient \bleu{`r} une valuation,
\bleu{a\in\textbf{Aexp}},  \bleu{X\in \textbf{Loc}}, \bleu{`s\in`S} et
\bleu{B} une expression booléenne de \bl{\textbf{Bexpv}}
\begin{eqnarraybleu}
  `s "|="^{`r}  \substit{B}{X}{a} & \textrm{ssi} &  `s[\Ainterp{a} `s
  /X] "|="^{`r} B  
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Correction (cas des instructions)}%
\verdir{Théorème :}  Si \bleu{"|-" \prepost{A}{c}{B}} alors  \bleu{"|="
  \prepost{A}{c}{B}}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Correction (cas des instructions)}%
\verdir{Théorème :}  Si \bleu{"|-" \prepost{A}{c}{B}} alors  \bleu{"|="
  \prepost{A}{c}{B}}.

\brunir{Démonstration :} 

La démonstration se fait par induction sur la preuve de \bleu{"|-"
  \prepost{A}{c}{B}}.

\begin{itemize}
\item \textit{Correction de {\textbf{skip}}}.  Dans ce cas,
  $\rouge{A}`=\rouge{B}$ \\ %
  et on a \bleu{"|-"\prepost{A}{\textbf{skip}}{A}}.  \\%
  Comme \bleu{\Cinterp{\textbf{skip}}`s  = `s},   clairement
  \begin{displaymathbleu}
    `s "|="^{`r} A \quad "=>"\quad \Cinterp{\textbf{skip}}`s "|="^{`r} A
  \end{displaymathbleu}
  donc \bleu{"|="\prepost{A}{\textbf{skip}}{A}}.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Correction (cas des instructions)}%
\begin{itemize}
\item \textit{Correction de l'affectation}.  Si \bleu{c} est
  \bleu{X:=a} alors $\rouge{A} `=
  \rouge{\substit{B}{X}{a}}$.

Comme on a \bleu{`s "|="^{`r}
    \substit{B}{X}{a}} ssi   \bleu{`s[\Ainterp{a} `s/X] "|="^{`r}
       B},  \ali (par le lemme précédent). \\
alors
  clairement 
  \begin{eqnarraybleu}
    `s "|="^{`r}  \substit{B}{X}{a} & "=>" &  \Cinterp{X:=a} `s "|="^{`r} B  
  \end{eqnarraybleu}
donc \bleu{"|=" \prepost{\substit{B}{X}{a}}{X:=A}{B}}.
\end{itemize}
\vfill \addtocounter{slide}{-1}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Correction (cas des instructions)}%

\begin{itemize}
  
\item \textit{Correction de la composition séquentielle}.\\
  Supposons \bleu{"|-" \prepost{A}{c_0;c_1}{B}}, alors il existe $\emph{C}$\\
  telle que \bleu{"|-" \prepost{A}{c_0}{C}} et \bleu{"|-"
    \prepost{C}{c_1}{B}}\\ et par induction,
  \bleu{"|=" \prepost{A}{c_0}{C}} et \bleu{"|=" \prepost{C}{c_1}{B}}.\\
  Soit \bleu{`r} une valuation quelconque et \bleu{`s} un état tel que
  \bleu{`s"|="^{`r} A} .  \\
  Parce que \bleu{"|="^{`r}
    \prepost{A}{c_0}{C}}, on a \bleu{\Cinterp{c_0}`s"|="^{`r} C} \\
  duquel associé à \bleu{"|="^{`r} \prepost{C}{c_1}{B}} on tire
  \bleu{\Cinterp{c_1}(\Cinterp{c_0}`s)"|="^{`r} B}, c'est-à-dire
  \bleu{\Cinterp{c_0;c_1}`s "|="^{`r} B} (par définition de \bleu{\Cinterp{\_}{}}).

  Donc \bleu{"|=" \prepost{A}{c_0;c_1}{B}}.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Correction (cas des instructions)} %
\begin{itemize}
  
\item \textit{Correction de la composition conditionnelle}.  En exercice !
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Correction (cas des instructions)}%
\begin{itemize}
  
\item \textit{Correction de la boucle}. \\
 Supposons que \bleu{"|-"
    \prepost{A}{\while{b}{c'}}{B}}.\\

On a forcément \bleu{\rouge{B} `= \rouge{A \wedge \neg b}}.\\

  On a aussi 
  \bleu{"|-"\prepost{A\wedge b}{c'}{A}}.  \\
  Donc \bleu{"|="\prepost{A\wedge b}{c'}{A}}.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  On va démontrer \bleu{P(n)} par induction sur \bleu{n}, où
  \begin{displaymathbleu}
    P(n) \qquad \rouge{\triangleq} \qquad (`A `s \in `S)\quad  `s "|="^{`r} A \quad "=>" \quad `G_{\Cinterp{c'}}^n(\bot)(`s)
    "|="^{`r} A \wedge \neg b.
  \end{displaymathbleu}
Il s'ensuivra que 
\begin{displaymathbleu}
`s "|="^{`r} A \quad "=>" \quad \Cinterp{\while{b}{c'}}(`s) "|="^{`r} A \wedge \neg b.
\end{displaymathbleu}
et donc \bleu{"|="\prepost{A}{\while{b}{c'}}{A \wedge \neg b}} 
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Correction (cas des instructions)}%
Preuve de \bleu{
    (`A `s \in `S)\quad  `s "|="^{`r} A \quad "=>" \quad `G_{\Cinterp{c'}}^n(\bot)(`s)
    "|="^{`r} A \wedge \neg b.}

$\bullet$ Si \bleu{n=0} alors \bleu{`G_{\Cinterp{c'}}^n(\bot)(`s) =
  \bot(`s) = \bot}\\
    donc \bleu{`G_{\Cinterp{c'}}^n(\bot)(`s) "|="^{`r} A \wedge \neg b}.
    
    $\bullet$ Rappelons que \bleu{`G_{\Cinterp{c'}}^{n+1}(\bot)} est
    défini sur les états \bleu{`s} tels que
\begin{itemize}
\item \bleu{\Cinterp{c'}^{i}`s} est défini pour \bleu{i``<= n+ 1}
\item et \bleu{\Binterp{b} (\Cinterp{c'}^{i}`s) = \textbf{true}} pour \bleu{i``<= n},
  tandis que \bleu{ \Binterp{b} (\Cinterp{c'}^{n+1}`s) = \textbf{false}}.
\end{itemize}

Et on a 
\begin{eqnarraybleu}
  `G_{\Cinterp{c'}}^{n+1}(\bot)(`s) &=& \Cinterp{c'}^{n+1}`s.
\end{eqnarraybleu}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Correction (cas des instructions)}%

D'où on tire \bleu{\Cinterp{c'}^{n+1}(`s) "|="^{`r}
  \neg b}, par définition de \bleu{\Cinterp{\_}{}}.  \\%
D'autre part par induction 
\begin{displaymathbleu}
  \Cinterp{c'}(`s) "|="^{`r} A \quad "=>" \quad \Cinterp{c'}^{n+1}(`s) "|="^{`r} A
\end{displaymathbleu}
Or par hypothèse \bleu{"|="\prepost{A\wedge b}{c'}{A}},\\
donc \bleu{`s' "|="^{`r} A} et
\bleu{\Binterp{b}`s'} impliquent \bleu{ \Cinterp{c'}(`s') "|="^{`r} A}.\\
Donc \bleu{ `s "|="^{`r} A ~"=>"~\Cinterp{c'}^{n+1}(`s) "|="^{`r} A}.

\medskip

D'autre part, \bleu{\neg \Binterp{b} \Cinterp{c'}^{n+1}`s} signifie
\bleu{\Cinterp{c'}^{n+1}(`s) "|="^{`r} \neg b}.

\medskip

Donc \bleu{ `s "|="^{`r} A ~"=>"~\Cinterp{c'}^{n+1}(`s) "|="^{`r} A
  \wedge \neg b}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Correction (cas des instructions)}%
\begin{itemize}
  
\item \textit{Correction de la règle de conséquence}.  Supposons
  qu'on ait 
  \begin{itemize}
  \item \bleu{"|=" A "=>" A'}, 
  \item \bleu{"|-"\prepost{A'}{c}{B'}} \quad donc par induction \quad  \bleu{"|="\prepost{A'}{c}{B'}} 
  \item et \bleu{"|=" B' "=>" B}.
\end{itemize}
Soit une valuation \bleu{`r}.  Supposons
  qu'on ait \bleu{`s "|="^{`r} A}, alors \bleu{`s "|="^{`r} A'}.   

  Donc \bleu{\Cinterp{c}`s "|="^{`r} B'}, donc aussi
  \bleu{\Cinterp{c}`s "|="^{`r} B}.  
  
  Par conséquent \bleu{"|="\prepost{A}{c}{B}}.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{vertfonce}{\textit{Complétude de la sémantique
          axiomatique }} }
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Précondition la plus faible}
Quand on veut prouver \bleu{\prepost{A}{c_0; c_1}{B}}, la question se pose de
savoir si on peut trouver une assertion  \emph{$C$} à mettre au milieu\\ c'est-à-dire
tel que \bleu{\prepost{A}{c_0}{C}} et \bleu{\prepost{C}{c_1}{B}}.  

L'idée c'est de la construire comme la \emph{précondition la plus faible}
associée à \bleu{B} et à l'instruction \bleu{c_1}.  
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Précondition la plus faible}
Tout d'abord on définit un ensemble d'états (pas une assertion!):
\begin{displaymathbleu}
 \wp{c}{B} =^{def} \{`s \in `S_\bot ~|~ \Cinterp{c}`s "|="^{`r} B\}.
\end{displaymathbleu}

C'est-à-dire l'image inverse par la fonction \bleu{\Cinterp{c}}  de
l'ensemble
\begin{displaymathbleu}
  \{`s' \in `S_\bot ~|~ `s' "|="^{`r} B\}.
\end{displaymathbleu}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Précondition la plus faible}
Supposons qu'il existe une assertion \bleu{A_0} telle que pour toute
valuation \bleu{`r}, on ait \bleu{\set{`s`:`S}{`s"|="^{`r}A_0} = \wp{c}{B}}.

Alors 
\begin{displaymathbleu}
  "|="^{`r} \prepost{A}{c}{B} \quad \textrm{ssi}   "|="^{`r} A "=>" A_0
\end{displaymathbleu}
autrement dit 
\begin{displaymathbleu}
  "|=" \prepost{A}{c}{B} \quad \textrm{ssi}   "|=" A "=>" A_0
\end{displaymathbleu}

Avec la règle de conséquence on devrait pouvoir construire les preuves
de correction partielle d'un programme.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Expressivité} %
  Un langage d'assertions est \emph{expressif} si \\ pour toute
  instruction \bleu{c} et toute assertion \bleu{B} \\il existe une
  assertion, notée \bleu{ w\llbracket c, B\rrbracket}, telle que \ali
  pour toute valuation~\bleu{`r} on ait
  \begin{displaymathbleu}
    \set{`s`:`S}{`s"|="^{`r} w\llbracket c,
    B\rrbracket} = \wp{c}{B}
  \end{displaymathbleu}

\bigskip

\emph{Attention:}  \bleu{ w\llbracket c, B\rrbracket} est une
expression du langage, alors que \bleu{\wp{c}{B}} est un sous-ensemble
de \bleu{`S}.
    \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Expressivité}
\verdir{Théorème :} \bleu{\textbf{Aexpv}} est expressif.

\brunir{Démonstration :} 

On l'obtient au prix de codages à la G\"odel.  

Voyez le livre de Glynn Winskel \emph{The Formal semantics of
  programming language}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Complétude}
Les règles de la sémantique axiomatique forment un système complet.

\verdir{Théorème :} (Cook) Si \bleu{"|=" \prepost{A}{c}{B}} alors  \bleu{"|-"
  \prepost{A}{c}{B}}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Complétude}
\brunir{Démonstration :}  En gros on arrive à montrer que 
\begin{displaymathbleu}
  "|=" \prepost{A}{c}{B}
\end{displaymathbleu}
implique 
\begin{displaymathbleu}
  "|-" \prepost{w\llbracket c, B\rrbracket}{c}{B}
\end{displaymathbleu}
où \bleu{w\llbracket c,
    B\rrbracket} est une assertion qui exprime la précondition la
  plus faible, associée à \bleu{B} et à  \bleu{c}.

On peut aussi montrer \bleu{"|=" A "=>" w\llbracket c,
    B\rrbracket}.
  
  Et donc on conclut par la règle de conséquence.  \vfill
\end{slide}
%======================================================
\end{document}
% LocalWords:  IMP Loc Aexp Bexp Com true false while fix faudrait-il d'IMP Pre
% LocalWords:  snapshot Floyd d'invariant s'écriront s'écrirait L'assertion iff
% LocalWords:  s'énoncer Intvar valuation McCarthy d'assertions ssi Post r-y qu
% LocalWords:  précondition postcondition Aexpv Bexpv skip WB Assn odel Glynn
% LocalWords:  Winskel
