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, 2010-2011.

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

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 acalculabilité. 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 , une version anglaise, plus complète, est également disponible.

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 14 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

 (forall number point : Type,
  forall perp_bisector : point -> point -> point -> Prop,
  forall distance : point -> point -> number,
  (forall a b c, perp_bisector a b c <-> distance a c = distance b c)
  ->
  forall a b c d, perp_bisector a b d -> perp_bisector b c d ->
   perp_bisector a c d)

TD pour la troisième semaine

Voir à la page suivante.

Devoir à la maison à faire avant le 28 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

Pas de TD cette semaine.

Devoir à la maison pour le 6 mars 2012

On considère l'expression arithmétique suivante:

aplus (aplus (avar "x") (avar "y")) (aplus (avar "z") (anum (-1)))

On désire évaluer cette expression dans l'environnement

(("x",1)::("y",2)::("z",3)::nil)

Quelle sera la valeur retournée? écrire une preuve Coq qui le démontre. On devra travailler avec les définitions suivantes:

Require Export ZArith String List.
Open Scope Z_scope.
Open Scope string_scope.

Inductive aexpr : Type :=
  avar (s:string) | anum (x:Z) | aplus (e1 e2 : aexpr).

Definition env := list (string * Z).

Inductive aeval : env -> aexpr -> Z -> Prop :=
  ae_num : forall r n, aeval r (anum n) n
| ae_var1 : forall r x v, aeval ((x,v)::r) (avar x) v
| ae_var2 : forall r x y v v' , x <> y -> aeval r (avar x) v' ->
              aeval ((y,v)::r) (avar x) v'
| ae_plus : forall r e1 e2 v1 v2,
              aeval r e1 v1 -> aeval r e2 v2 ->
              aeval r (aplus e1 e2) (v1 + v2).

TD pour la cinquième semaine

Voir à la page suivante

TD du 27 mars 2012

Voir à la page suivante

Examen sur table du 3 avril 2012

Le sujet et la solution sont maintenant disponibles.