\documentclass{article}

\usepackage{fancybox}
\usepackage{a4}
\usepackage[latin1]{inputenc}
\usepackage[francais]{babel}
\usepackage[all]{xy}
\usepackage{pslatex}
\usepackage{qsymbols}
\usepackage{amsfonts,amsmath,amsthm,amssymb,stmaryrd}

\newcommand{\R}{\mathbb{R}}
\newcommand{\N}{\mathbb{N}}
\newcommand{\A}{\ensuremath{\bl{\cal A}}}
\newcommand{\M}{{\cal M}}
\newcommand{\C}{{\cal C}}
\newcommand{\interp}[2]{\llbracket#1\rrbracket^{#2}}

\newcommand{\Invar}{\mathsf{p} = (\mathsf{i}`* \mathsf{i} `* \mathsf{i})\quad \wedge \quad \mathsf{q} = (3 `*
    \mathsf{i} `* \mathsf{i}) +   (3 `* \mathsf{i}) \quad \wedge \quad
  \mathsf{i} \le \mathsf{n}}
\newcommand{\Pre}[1]{\mathbf{Pre_{#1}}}
\newcommand{\Post}[1]{\mathbf{Post_{#1}}}

%% ==============================================================
%%                   Reductions and other relations
%% ==============================================================

\newcommand{\ra}{\xymatrix{\ar@{>}[r] &}}
\newcommand{\ranorm}{\xymatrix{\ar@{>>|}[r] &}}
\newcommand{\rara}{\xymatrix{\ar@{>>}[r] &}}
\newcommand{\longequiv}{\xymatrix{\ar@3{-}[r] &}}
\newcommand{\la}{\xymatrix{\ar@{<-}[r] &}}
\newcommand{\llbda}{\mathbf{\lambda\hspace{-.65em}\lambda}}
\newcommand{\w}{\interp{`l x . x x}{D_A}}
%% <...> are angle brackets.
\mathcode`\<=\string"4268 \mathcode`\>=\string"5269 %

\title{Magistère d'Informatique et Modélisation}
\author{Corrigé de sémantique}

\date{8 janvier 2003}

\begin{document}
\maketitle 
\thispagestyle{empty}

\section*{Exercice 1}

Il faut calculer $\w = G(\llbda d F(d)(d))$.  Tout d'abord on note que
\begin{eqnarray*}
  F(d) (d) &=& \{b ~|~ (\exists `b \subseteq d) ~ (`b,b)\in d\}
\end{eqnarray*}
donc 
\begin{eqnarray*}
  \w &=& G(\llbda d . F(d)(d)) \\
  & =& \{(`g,c) ~|~ c\in\{b~|~ (\exists `b \subseteq
  `g)~(`b,b)\in `g\}\}\\
  &=&  \{(`g,c) ~|~ (\exists `b \subseteq `g)~(`b,c)\in `g\}
\end{eqnarray*}
Finalement on a 
\begin{eqnarray*}
  F(\w)(\w) & = & \{d ~|~ (\exists `d\subseteq \w) ~ (`d,d)\in \w\}\\
  &=& \{ d~|~ (\exists `d \subseteq \w) ~ (\exists `b \subseteq
                                             `d)~(`b, d) \in`d\}\\
  &=& \{ d~|~ (\exists `d \subseteq B)(`E `b \subseteq d)~
  (`b, d) \in `d  \wedge (d \mathrm{~fini})   %
  \\ && \hspace*{100pt} \wedge \
  [(`g, c) \in `d "=>" (`E `z \subseteq `g)~(`z,  c)\in `g] \}.
\end{eqnarray*}

\section*{Exercice 2}

\begin{enumerate}
\item Le programme qui calcule le cube est $\mathcal{P}_2$.
\item Une postcondition est $\mathsf{p} = \mathsf{n}^3$. Pour l'écrire
  dans le langage \textsf{\textbf{Aexp}} des expressions arithmétiques
  de \textsf{IMP}, on peut considérer $\mathsf{n}`*\mathsf{n}`*\mathsf{n}$
  au lieu $\mathsf{n}^3$.
\item Un invariant de la boucle est 
\[\Invar.\]
Les étapes de la figure~\ref{fig:boucle} permettent de  prouver 

\begin{math}
  \begin{sf}
\Pre{} :  \Invar \quad \wedge \quad \mathsf{i} < \mathsf{n}\\
  \hspace*{24pt} p := p + q + 1 ; \\
  \hspace*{24pt} i := i + 1 ; \\
  \hspace*{24pt} q := q + (6 `* i)\\
\Post{} :  \Invar
  \end{sf}
\end{math}

\begin{figure}[htbp]
\doublebox{
  \begin{math}
  \begin{array}{l}
    \Pre{} :  \Invar \quad \wedge \quad \mathsf{i} < \mathsf{n}\\[12pt]
%
    \Pre{1} : \mathsf{p + \mathsf{q} + 1} = (\mathsf{i}`* \mathsf{i} `*
    \mathsf{i}) + (3 `* \mathsf{i} `* \mathsf{i}) + (3 `* \mathsf{i}) + 1 \quad \wedge \quad
    \mathsf{q} = (3 `* \mathsf{i} `* \mathsf{i}) + (3 `* \mathsf{i})
    \quad \wedge \quad
    \mathsf{i} < \mathsf{n}\\
    \hspace*{24pt} \mathsf{p} := \mathsf{p} + \mathsf{q} + 1 ; \\
    \Post{1} : \mathsf{p} = (\mathsf{i}`* \mathsf{i} `* \mathsf{i}) +
    (3 `* \mathsf{i} `* \mathsf{i}) + (3 `* \mathsf{i}) + 1 \quad \wedge \quad \mathsf{q} = (3 `*
    \mathsf{i} `* \mathsf{i}) +   (3 `* \mathsf{i})  \quad \wedge \quad
  \mathsf{i} < \mathsf{n}\\[12pt]
%
    \Pre{2} : \mathsf{p} = \mathsf{(i+1)}`* \mathsf{(i+1)} `*
    \mathsf{(i+1)}\quad \wedge \quad \mathsf{q} = (3 `*
    \mathsf{(i+1)} `* \mathsf{(i+1)}) -   (3 `* \mathsf{(i+1)}) \\
    \hspace*{100pt}\wedge \quad \mathsf{i+1} \le \mathsf{n}\\
    \hspace*{24pt} \mathsf{i} := \mathsf{i} + 1 ; \\
    \Post{2} : \mathsf{p} = (\mathsf{i}`* \mathsf{i} `* \mathsf{i})\quad
    \wedge \quad \mathsf{q} = (3 `*
    \mathsf{i} `* \mathsf{i}) -   (3 `* \mathsf{i})  \quad \wedge \quad
  \mathsf{i} \le \mathsf{n}\\[12pt]
%
    \Pre{3} : \mathsf{p} = (\mathsf{i}`* \mathsf{i} `* \mathsf{i})\quad
    \wedge \quad \mathsf{q + (6 `* \mathsf{i})} = (3 `* \mathsf{i} `*
    \mathsf{i}) + (3 `* \mathsf{i}) \quad \wedge \quad
  \mathsf{i} \le \mathsf{n}\\
    \hspace*{24pt} \mathsf{q} := \mathsf{q} + (6 `* \mathsf{i})\\
    \Post{3} : \Invar
\end{array}
  \end{math}
}
\caption{Les trois affectations de la boucle}
\label{fig:boucle}
\end{figure}

On voit que $\Pre{} "=>" \Pre{0}$, que $\Pre{0} "=>" \Pre{1}$, que
$\Post{1} "=>" \Pre{2}$ et que $\Post{2} "=>" \Pre{3}$, ce qui permet
d'appliquer trois fois la \emph{règle de conséquence}. De plus
$\Post{3} `= \Post{}$.  Les conditions $\Pre{i}$ et $\Post{i}$ sont
chaque fois des applications de la \emph{règle d'affectation}.

En application de la \emph{règle de la boucle}, on a 
\begin{displaymath}
  \Invar \quad \wedge \quad \neg (\mathsf{i} < \mathsf{n}).
\end{displaymath}
ce qui implique clairement
\begin{displaymath}
  \mathsf{q} = \mathsf{n} `*\mathsf{n} `*\mathsf{n}.
\end{displaymath}
Reste à prouver que l'invariant est une postcondition des trois
premières instructions (voir figure~\ref{fig:premieres}).  La
précondition de ces trois affectations qui correspond à $\Invar$ est
$0 = (0`* 0 `* 0)\quad \wedge \quad 0 = (3 `* 0 `* 0) + (3 `* 0) \quad
\wedge \quad 0 \le \mathsf{n}$ qui est clairement vraie.
\begin{figure}[htbp]
\doublebox{
  \begin{math}
    \begin{array}{l}
    true\\
    \hspace*{24pt} \mathsf{p} := 0 ; \\
    \hspace*{24pt} \mathsf{q} := 0 ; \\
    \hspace*{24pt} \mathsf{i} := 0 ; \\
    \textsf{Init} : \Invar
  \end{array}
\end{math}
}
  \caption{Les trois premières affectations}
  \label{fig:premieres}
\end{figure}

\end{enumerate}

\section*{Exercice 3}
Pour la question 1, un système possible est:

\newcommand{\rien}{\textsf{Rien}}
\newcommand{\tout}{\textsf{Tout}}
\newcommand{\rapu}{\textsf{rapide1}}
\newcommand{\rapd}{\textsf{rapide2}}
\newcommand{\rapubar}{\overline{\textsf{rapide1}}}
\newcommand{\rapdbar}{\overline{\textsf{rapide2}}}
\newcommand{\libu}{\textsf{libere1}}
\newcommand{\libd}{\textsf{libere2}}
\newcommand{\libubar}{\overline{\textsf{libere1}}}
\newcommand{\libdbar}{\overline{\textsf{libere2}}}

\begin{eqnarray*}
  \mathsf{SERVEUR} &=& \rien ~|~ \mathsf{A}~|~ \mathsf{B} ~|~ \mathsf{C}\\
  \rien &=& \mathsf{requete}(x).\bar{x}<\rapu,\libu> . \mathsf{R1}\\
  \mathsf{R1} &=& \mathsf{requete}(x) . \bar{x} <\rapd,\libd> . \tout ~|~
  \rapubar . \libubar . \rien\\
  \mathsf{R2} &=& \mathsf{requete}(x) . \bar{x} <\rapu,\libu> . \tout ~|~
  \rapdbar . \libdbar . \rien \\
  \tout &=& \rapubar .\libubar . \mathsf{R1} %
          ~|~ \rapdbar. \libdbar . \mathsf{R2} \\
  \mathsf{A} &=& \overline{\mathsf{requete}}<a> . a(y,z) . y . z \\
  \mathsf{B} &=& \overline{\mathsf{requete}}<b> . b(y,z) . y . z \\
  \mathsf{C} &=& \overline{\mathsf{requete}}<c> . c(y,z) . y . z 
\end{eqnarray*}

Pour la question 2, 
\begin{eqnarray*}
  \mathsf{SERVEUR} &"->"& \bar{a}<\rapu, \libu>.\mathsf{R1} ~|~
  a(y,z).y.z ~|~ \mathsf{B} ~|~ \mathsf{C}\\
  &"->"& \mathsf{R1} ~|~ \rapu . \libu ~|~ \mathsf{B} ~|~ \mathsf{C}\\
  &"->"& \bar{b}<\rapd,\libd> . \tout %
      ~|~ \rapu . \libu  ~|~ b(y,z) . y . z ~|~ \mathsf{C}\\
  &"->"& \tout ~|~ \rapu . \libu  ~|~ \rapd .\libd ~|~ \mathsf{C}\\
  &=& \rapubar . \libubar . \mathsf{R1} ~|~ \rapdbar. \libdbar . \mathsf{R2} 
          ~|~ \rapu . \libu  ~|~ \rapd .\libd ~|~ \mathsf{C}\\
  &"->"& \rapubar . \libubar . \mathsf{R1} ~|~ \libdbar . \mathsf{R2} 
          ~|~ \rapu . \libu  ~|~ \libd ~|~ \mathsf{C}\\
  &"->"& \rapubar . \libubar . \mathsf{R1} ~|~ \mathsf{R2} 
          ~|~ \rapu . \libu ~|~ \mathsf{C}\\
 \end{eqnarray*}

\end{document}
