\documentclass{article}

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

%% ==============================================================
%%                   Réductions et autres relations
%% ==============================================================

\newcommand{\Nat}{\mathbb{N}}
\newcommand{\interp}[2]{\llbracket#1\rrbracket^{#2}}

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

\date{2003}

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

\section*{Exercice 1}

On rappelle que le modèle d'Engeler est une rétraction sur l'ensemble
$D_A = {\cal P}(B)$ où $A$ ne contient pas d'éléments $(`b,b)\in B$ et
où $B$ est défini ainsi.
\begin{eqnarray*}
      B_0  & = &  A \\
    B_{n+1}  & = &  B_n \cup \{(`b,b) ~|~ b\in B_n \wedge `b \subseteq
    B_n \wedge `b \textrm{~est fini}\},\\
    B  & = &  \bigcup_{n\in \Nat} B_n.
 \end{eqnarray*}
On définit $F: D_A \rightarrow [D_A \rightarrow D_A]$ et %
$G: [D_A \rightarrow D_A] \rightarrow D_A$ par
\begin{eqnarray*}
    F(x)(y) & = & \{b ~|~  (\exists `b \subseteq y) \quad (`b, b) \in x\}\\
    G(f) & = & \{(`b, b) ~|~ b \in f(`b)\}.
  \end{eqnarray*}
  \begin{enumerate}
  \item Calculer $\interp{`l x . x x}{D_A}$.
  \item Calculer $\interp{(`l x . x x)~(`l x . x x)}{D_A}$.
  \end{enumerate}

\section*{Exercice 2}

On considère les programmes \textsf{IMP}

\vspace*{12pt}

%   P1
%  p := 0 ; 
%  q := 0 ; 
%  i := 0 ; 
%    while i < n do
%    p := p + q + 1 ; 
%    q := q + (6 * i)  ; 
%    i := i + 1

%  P2
%  p := 0 ; 
%  q := 0 ; 
%  i := 0 ; 
%    while i < n do
%    p := p + q + 1 ; 
%    i := i + 1 ;
%    q := q + (6 * i)  

\centerline{
\begin{math}
\begin{sf}
\mathcal{P}_1 =  \left\{
\begin{array}{l}
  p := 0 ; \\
  q := 0 ; \\
  i := 0 ; \\
  \mathbf{while}\quad i < n \quad \mathbf{do} \\
  \hspace*{24pt} p := p + q + 1 ; \\
  \hspace*{24pt} q := q + (6 `* i)  ; \\
  \hspace*{24pt} i := i + 1
\end{array}
\right. \hfill
\mathcal{P}_2 =  \left\{
\begin{array}{l}
  p := 0 ; \\
  q := 0 ; \\
  i := 0 ; \\
  \mathbf{while}\quad i < n \quad \mathbf{do} \\
  \hspace*{24pt} p := p + q + 1 ; \\
  \hspace*{24pt} i := i + 1 ; \\
  \hspace*{24pt} q := q + (6 `* i)
\end{array}
\right.
\end{sf}
\end{math}
}

\begin{enumerate}
\item Lequel de ces programmes calcule le cube de $n$ ?
\item Quelle est une postcondition satisfaite par ce programme qui
  garantit ce fait ?
\item Démontrer rigoureusement cette propriété en utilisant les règles
  de la sémantique axiomatique.
\end{enumerate}


\section*{Exercice 3}

On veut décrire en $`p$-calcul, un système de trois clients
\textsf{A}, \textsf{B} et \textsf{C} qui envoient à un serveur désigné
\textsf{SERVEUR} des masses de données par deux liaisons rapides
désignées par \textsf{rapide1} et \textsf{rapide2} qu'ils doivent se
partager.  Pour cela, les clients font des requêtes au serveur 
\emph{par un canal \textsf{lent}} 
et se voient attribuer une liaison rapide 
lorsque c'est possible, selon une politique d'attribution aléatoire

Les clients avertissent le serveur quand ils libèrent la liaison rapide qui 
leur a été attribuée.

\begin{enumerate}
\item Décrivez en $`p$-calcul ce protocole, autrement dit donnez les
  équations du processus \textsf{Serveur} et des processus
  \textsf{Client}($x$).
\item Décrivez les réductions qui correspondent à la suite d'actions
  (plus quelques actions intermédiaires éventuelles): 
  \begin{itemize}
  \item \textsf{A} obtient \textsf{rapide1}, 
  \item \textsf{B} obtient \textsf{rapide2},
  \item \textsf{B} libère \textsf{rapide2}.
  \end{itemize}
\item Modifier le protocole précédent afin  d'implanter une politique 
d'attribution "premier mis en attente, premier servi".

\end{enumerate}

\end{document}
