930.tex

\documentclass{agregfiche}

% V1 par Aliaume Lopez
% Relu par Charlie Jacomme
% Relu par David Baelde

\title{Leçon 930 -- Sémantique des langages de programmation. Exemples.}

\begin{document}

\maketitle

\secrapports

\begin{rapport}{2017,2018,2019}

    L’objectif est de formaliser ce qu’est un programme : introduction des
    sémantiques opérationnelle et dénotationnelle, dans le but de pouvoir faire
    des preuves de programmes, des preuves d’équivalence, des preuves de
    correction de traduction. Ces notions sont typiquement introduites sur un
    langage de programmation (impératif) jouet. On peut tout à fait se limiter à
    un langage qui ne nécessite pas l’introduction des CPOs et des théorèmes de
    point fixe généraux. En revanche, on s’attend ici à ce que les liens entre
    sémantique opérationnelle et dénotationnelle soient étudiés (toujours dans le
    cas d’un langage jouet). Il est aussi important que la leçon présente des
    exemples d’utilisation des notions introduites, comme des preuves
    d’équivalence de programmes ou des preuves de correction de programmes.

\end{rapport}

\secindispensables

\begin{itemize}
    \item Sémantique opérationnelle (petit/grand pas) et dénotationnelle des commandes de IMP.
    \item Équivalences entre les
        sémantiques.
     \item Exemples de programmes, avec une interprétation de leur
     correction dans une des sémantiques présentées ci-dessus.
\end{itemize}

\secasavoir

\begin{itemize}
	\item Utiliser la sémantique pour énoncer des propriétés : correction d'un
	programme, terminaison, validité d'une optimisation.
    \item Compositionnalité de la sémantique dénotationnelle, qui fait que l'équivalence est une congruence.
    \item Identifier les relations fonctionnelles ou totales.
\end{itemize}

\secidees

\begin{itemize}
\item Sémantique axiomatique (logique de Hoare).
\item Paresse dans les expressions booléennes et non terminaison.
\item Effets de bords dans les expressions.
\item Instructions break et continue (en petit pas ou axiomatique).

\end{itemize}
\secpieges

\begin{itemize}
    \item Dans IMP, seule la non terminaison empêche d'avoir un résultat dans la sémantique à grand pas (ou dénotationnelle), ce qui n'est pas toujours le cas. En toute généralité, la non terminaison se définit plutôt à petit pas.
    \item Définir les expressions comme des termes.
    \item On peut définir la sémantique dénotationelle du while simplement comme un sup, et ainsi éviter le formalisme des CPO.  Si on parle de point fixe, il faut connaître le théorème d'existence, et illustrer son intérêt. Par exemple, cela montre que le while et son déroulé ont la même sémantique.
    \item Bien faire attention aux références qui prennent des directions
      \emph{incompatibles} très tôt. Par exemple, si le domaine de définition
      des variables est $\mathbb{N}$ alors l'opération de soustraction
      doit être \emph{binaire}, alors que dans le cas de $\mathbb{Z}$ on peut
      se contenter d'une soustraction \emph{unaire}.
    \item Réfléchir aux liens avec d'autres leçons~:
      sémantique petit pas pour le lambda-calcul et les machines de Turing,
      sémantique dénotationnelle pour les expressions régulière (langage).
\end{itemize}


\secquestionsclassiques

\begin{itemize}
    \item Quel est l'intérêt des différentes sémantiques ?
    \item Quelles sémantiques permettent de définir une notion de complexité ?
%
%    \item Pour le programme d'une centrale nucléaire, quelle sémantique
%        paraît la plus adaptée ?
    \item Quelles sémantiques sont utilisées en pratique pour vérifier des programmes ?

    \item Quelle sémantique permet de vérifier un programme qui ne termine pas ?

    \item Peut-on faire un lien entre la sémantique dénotationnelle
        et la preuve de programme ?

    \item Calculer la sémantique dénotationnelle d'un programme
        avec une boucle while simple (division euclidienne, fibonacci...)
%    \item Conaissez-vous un langage pour lequel il n'y a pas
%        de théorème d'adéquation ? De théorème de correction ?
%
    \item Connaissez-vous un autre moyen de définir une sémantique ?
        (plus faible précondition)
    \item Vérifier la continuité de la fonction utilisée pour définir le WHILE ? (si il a été défini ainsi)
    \item Comment ajouter un choix non déterministe dans
        vos sémantiques ?
    \item Comment ajouter un choix probabiliste (pièce non biaisée par exemple)
        ?
        \item Est-ce que IMP est Turing-complet ? L'équivalence est-elle décidable ?
\end{itemize}

\secreferences

\begin{itemize}
\item \input{refs/winskel}
%\item \temporary{\url{http://www.cl.cam.ac.uk/~gw104/dens.pdf}}
%    (aussi Glynn Winskel)
\end{itemize}

\secdev

\begin{itemize}
\item[++]  \input{dev/semantiqueeoperdenotequiv}

\item[++]  \input{dev/semantiqueprogrammeequiv}

\item[+]   \input{dev/factorielhoare}

%\temporary{}
%\item[-] \temporary{Complétude de Hoare}
%Attention difficile

\end{itemize}


\end{document}