Le plan du cours change d'année en année. Vous pouvez accéder au cours tel que je l'avais fait (ou avais prévu de le faire) en 2000-2001, 2001-2002, 2002-2003, 2003-2004, 2004-2005, 2005-2006, 2006-2007, 2007-2008, 2008-2009, 2009-2010.

Cours de sémantique (année 2010-2011)

Dans ce cours nous voulons que les étudiants apprennent à réfléchir sur le sens des programmes et le pouvoir expressif des langages de programmation. Ce cours repose sur une fondation théorique importante: vous devrez maîtriser des notions de logique et de calculabilité. Mais les applications pratiques de ce cours sont spectaculaires: c'est grâce aux concepts abordés dans ce cours que l'on est capable de mettre au point du logiciel critique, utilisable en avionique, en commerce électronique, ou en transport ferroviaire. Une bonne maîtrise de la sémantique des langages de programmation permet en effet de développer des compilateurs auxquels on peut faire confiance, des outils de vérification automatique pour éviter les erreurs de débordement, les trous de sécurité, etc, et des outils pour spécifier le comportement attendu du logiciel et vérifier que les programmes respectent leurs spécifications.

1. apprentissage du système Coq (trois séances)

Dans la première partie du cours, nous apprendrons à nous servir d'un système de démonstration sur ordinateur. Nous utiliserons ensuite ce système de démonstration sur ordinateur pour décrire précisément un petit langage de programmation, pour développer des outils manipulant des programmes de ce langage de programmation, et pour montrer que ces outils sont corrects, au sens où il permettent d'éviter l'introduction d'erreurs de programmation ou de détecter certaines classes d'erreurs.

Les notes pour le premier cours sont disponibles ici .

TD pour la première semaine

Voir à la page suivante.

Devoir à la maison entre la première et la deuxième semaine

Construire une fonction qui prend en entrée une liste d'entiers et retourne une nouvelle liste contenant les mêmes nombres, mais sans duplications. Par exemple, si l'entrée est

1::3::3::2::2::4::nil

Alors le résultat peut être

1::2::3::4::nil

ou bien

1::3::2::4::nil

TD pour la deuxième semaine

Voir à la page suivante.

Devoir à la maison à faire avant le 15 février

Démontrez les énoncés suivant

 forall P Q: nat -> Prop,
   (forall x, P x -> Q (S x)) ->
   (forall x, Q x -> Q (S (S x))) ->
   (forall x, P x -> Q (S (S (S x))))

 (forall P : nat -> Prop,
     P 0 -> (forall x, P x -> P (S x)) ->
     forall n, P n) ->
 forall f: nat -> nat -> nat,
    (forall x, f x 0 = x) ->
    (forall x y, f x (S y) = S (f x y)) ->
    forall z, f 0 z = z

TD pour la troisième semaine

Voir à la page suivante.

Devoir à la maison à faire avant le 22 février

Etudier la tactique ring dans le manuel de référence de Coq, puis étudiez la définition suivante

Fixpoint f1 (n:nat) : nat :=
  match n with
    0 => 0
  | S p => 2 * p + 1 + f1 p
  end.

Prouvez le lemme suivant:

Require Import Arith.

Lemma f1_sq : forall n, f1 n = n * n.

1. Sémantique opérationnelle

Les notes pour le quatrième cours sont ici.

TD pour la quatrième semaine

Voir à la page suivante.

Devoir à la maison pour le 8 mars

On considère le programme suivant

while (blt (anum 0) (avar "x"))
  (sequence (assign "x" (aplus (avar "x") (anum (-1))))
            (assign "y" (aplus (avar "y") (avar "z"))))

Démontrez par récurrence sur n:nat que l'exécution de ce programme dans l'environnement

(("x", Z_of_nat n)::("y", 0)::("z", z)::nil)

termine et retourne l'environnement

(("x", 0)::("y", Z_of_nat n * z)::("z",z)::nil)

TD pour la cinquième semaine

Voir à la page suivante

Devoir à la maison pour le 8 mars

Démontrez l'énoncé suivant (en utilisant les mêmes définitions que pour le td

forall r x n r', update r x n r' ->
  forall r'', update r x n r'' -> r' = r''