Cours de L3 “programmation 1”

En général, voir l’emploi du temps.

L’examen a une forme un peu particulière:

  • Voici la première partie, qui vous servira à vous familiariser avec les notions, notations et règles. Voici un corrigé de cette première partie.
    La première partie n’est pas notée, mais on ne peut pas faire l’examen sans avoir fait la première partie.
  • Voici la deuxième partie; elle est formée de toutes les questions absentes de la première partie, et repérées par des ‘[…]’, et a été donnée lors de l’examen sur table du vendredi 19 janvier 2024.
  • Voici un corrigé possible de la deuxième partie.

Le contenu du cours

Le cours de programmation de 1ère année du l’année L3 se découpe en deux parties. Ceci est la page de la première partie. Elle-même se découpe en deux sous-parties.

De quoi sera-t-il question dans la première sous-partie?

  • des différents styles de langages de programmation, avec un accent particulier sur la programmation impérative (notamment en langage C), qui est sans doute relativement nouvelle pour vous. On parlera aussi de langages fonctionnels; il est probable que vous ayez déjà quelques bases en OCaml, mais on y parlera aussi de Lisp.
  • Il y sera aussi question des constructions typiques de chaque famille de langages, des questions de portée (lexicale, opposée à la liaison dynamique), de passage de paramètres, des constructions de types de données, etc.
  • A plus bas niveau, on verra comment tous ces objets sont représentés en machine, et le cours s’interfacera notamment avec celui d’architecture et systèmes de Stefan Schwoon.
  • On s’exercera aussi à écrire de petits programmes, et des moins petits, dans chacun de ces langages et chacun des styles permis ou encouragés dans ces langages. Ceci se fera en séances de TP, ou d’une séance de TP sur l’autre.

Tout ceci nous occupera, grosso modo, de septembre à novembre. Les cours y seront assurés par Mihaela Sighireanu.

Et dans la seconde sous-partie?

De novembre à début janvier, nous profiterons des acquis pour progresser vers:

  • la sémantique des langages de programmation, autrement dit la représentation mathématique de ce que les programmes font (ou devraient faire). On parlera notamment de sémantique opérationnelle à grands pas, et de sémantique dénotationnelle.
  • L’intérêt principal d’une formalisation mathématique est d’établir des théorèmes. On parlera donc de preuve sur des programmes, ou sur des propriétés de langage de programmation.
  • L’autre intérêt d’une sémantique est la documentation précise du langage. Dans le cadre du projet, on insistera donc sur le fait que le mini-compilateur de C que vous aurez à réaliser respecte la sémantique proposée.

Modalités d’examen

Les modalités d’examen sont grosso modo les suivantes. Elles prennent en compte les composantes suivantes:

  • D: partiel à mi-parcours (normalement en novembre), sous forme de devoir à la maison;
  • E: examen (janvier), portant essentiellement sur la seconde partie du cours, mais pas nécessairement exclusivement;
  • CC: contrôle continu, moyenne des 3 meilleurs rendus en TD (sur 6);
  • P1: projet 1, d’entraînement, en TP;
  • P2: projet 2, projet compilation.

La note finale sera:

0,4 E + 0,1 CC + 0,2 D + 0,1 P1 + 0,3 P2
à condition que P1 et P2 soient validés (≥10/20). Si P1 ou P2 n’est pas validé, le module ne pourra pas être validé.
En cas de non validation, une session 2 sera organisée, pour ceux qui la demandent; la note de session 2 se substituera alors à celle de session 1, et ne saura dépasser 10/20. La session 2 consistera en un projet de programmation supplémentaire sur le modèle de P2, et/ou des questions portant essentiellement sur la seconde partie du cours.

Voici le sujet d’examen 2021/22, et son corrigé, à titre d’exemple. De même, le sujet d’examen 2022/23, et son corrigé.

Le programme des cours

Ceci est un programme indicatif de la deuxième partie, sujet à évolution.

  • Sémantique 1: les notes de cours. Sémantiques opérationnelles d’un langage impératif jouet. Voici la première série de transparents de ce cours de sémantique, et la version courte.
  • Sémantique 2: les notes de cours. Sémantique dénotationnelle, dcpos, théorèmes de points fixes. Voici la deuxième série de transparents de ce cours de sémantique, et la version courte. La vidéo du cours (2020).
  • Sémantique 2, suite (mêmes notes de cours). Correction, adéquation, équivalence contextuelle, logique de Hoare, weakest preconditions. Voici la troisième série de transparents de ce cours de sémantique, et la version courte… mais nous terminerons d’abord la deuxième série. La vidéo de ce cours (2020).
  • Sémantique 2, fin (mêmes notes de cours). Le langage fonctionnel d’ordre supérieur PCF, sémantiques opérationnelle dénotationnelle, clôtures, correction, adéquation. Voici la quatrième série de transparents de ce cours de sémantique, et la version courte. La vidéo de ce cours (2020): nous nous sommes arrêtés au transparent 7 de cette dernière série de transparents.
  • Sémantique 3: les notes de cours. Typage, et plus spécifiquement de ML; l’algorithme d’inférence de Hindley pour ML monomorphe, le problème de l’unification. La vidéo (2020); nous n’avions pas encore commencé à parler de typage, qui est traitée dans la vidéo suivante. Les transparents, et la version courte.
  • Sémantique 3, suite. La vidéo (2020). Termes, substitutions, l’algorithme d’unification, sa correction, unificateurs les plus généraux (mgu).
  • Sémantique 3, fin. Unification, fin: terminaison; théorème de Milner (“well-typed programs do not go Wrong”), algorithme W et typage de ML polymorphe. La vidéo (2020).
  • Optionnel: les bases de l’interprétation abstraite, la théorie qui sous-tend l’analyse statique de programmes, avec les transparents, et la version courte. La vidéo (2020).