Université du Québec en Outaouais Département d'informatique et d'ingénierie
Sigle : INF4133  Gr. 01
Titre : Aspects logiques de la programmation
Session : Hiver 2007   Horaire et local
Professeur : Sami, Yamina
1. Description du cours paraissant à l'annuaire :

Objectifs

Fournir à l'étudiant un ensemble des techniques théoriques et pratiques qui sont utilisées dans le développement des programmes et à leur preuve.

Contenu

Logique du premier ordre. Structures et satisfaction des formules. Formules prénexes et formes normales. Formes de Skolem. Déduction et complétude dans la logique du premier ordre. Démonstration automatique : unification, méthodes de résolution. Théorie des modèles de calcul : modèles séquentiels, modèles non déterministes et modèles à accès aléatoire. Développement des programmes. Sémantiques de certaines constructions : affectation, structures alternatives, structures itératives. Le développement de procédures abstraites : invariants, terminaison, récursivité, efficacité. Théorie de la preuve : prouvabilité, consistance, déduction. Fonctions récursives.
2. Objectifs spécifiques du cours :
Ce cours introduit un ensemble de techniques théoriques et pratiques qui sont utilisées dans le développement des programmes et à leur preuve. Après avoir suivi ce cours, l'étudiant connaîtra les éléments de base de la programmation logique, la syntaxe et la sémantique de la logique propositionnelle et du calcul des prédicats du premier ordre et le développement des programmes à partir de formules logiques.
3. Stratégies pédagogiques :
Les formules pédagogiques suivantes seront utilisées :
  • L'enseignement est dispensé sous forme magistrale.
  • Des démonstrations viennent illustrer certaines notions théoriques.
  • Des séries d’exercices avec solutionnaires se rapportant directement aux exposés compléteront l'apprentissage.
  • Un examen de mi-session et un examen final.
4. Heures de disponibilité ou modalités pour rendez-vous :
Les consultations sont possibles le mardi de 15h30mn à 16h30mn.
5. Plan détaillé du cours sur 15 semaines :
Semaine Thèmes Dates
1    Rappels sur la logique propositionnelle.
  • Langage propositionnel.
  • Sémantique.
  • Formes normales.
 09 jan. 2007 
2    Langages du premier ordre.
  • Construction des termes.
  • Construction des formules.
  • Variables libres et variables liées.
 16 jan. 2007 
3    Sémantique de la logique du premier ordre.
  • Structures et langages.
  • Structures et satisfaction des formules.
  • Formules valides.
  • Formules équivalentes.
  • Substitution.
 23 jan. 2007 
4    Formules prénexes et formes normales. Formes de Skolem.

Déduction et complétude de la logique du premier ordre.

  • Système de déduction.
  • Déduction et validité.
  • Déduction et complétude.

Quiz1.

30 jan. 2007 
5    Résolution.
  • Mise sous forme de clauses.
  • Unification.
  • Méthode de résolution.
  • Modèles de Herbrand
  • La programmation logique.
 06 fév. 2007 
6    Syntaxe et signification des programmes Prolog.
  • Introduction.
  • Données.
  • Unification.
  • Sens déclaratif des programmes Prolog.
  • Sens procédural des programmes Prolog.
  • Étude de cas: Le singe et les bananes.

Affichage du Devoir1.

13 fév. 2007 
7    Introduction à la preuve de correction des programmes par la présentation d’un problème de manière informelle.
  • Définition du problème, solution et preuve de correction.

L’utilisation des assertions pour la documentation des programmes.

Sémantique d’un langage minimal (1).

  • Préliminaires.
  • Le prédicat transformateur.
  • Les commandes skip, abort et la composition.

 20 fév. 2007 
8    Semaine d'études.
  • Séance de révision.
  • Remise du Devoir1.
27 fév. 2007 
9   
  • Examen de mi-session.
 06 mars 2007 
10    Sémantique d'un langage minimal (2).
  • La commande d'affectation.
  • La commande alternative.
  • La commande itérative.
 13 mars 2007 
11    Développement des programmes.
  • Le développement des boucles à partir d'invariants et de limites.
  • Le développement d'invariants

Études de cas : Algorithmes de tri et de recherche.

  • Le drapeau national Danois : définition du problème, solution et vérification de la solution.
  • Recherche des K plus petites valeurs : Spécification et algorithme.

 20 mars 2007 
12    L’utilisation de l’itération au lieu de la récursivité.
  • Résolution des problèmes simples dans une première étape.
  • Diviser et conquérir.
  • Parcours d’un arbre binaire.

Quiz2

 27 mars 2007 
13    Des considérations d’efficacité.
  • Restriction du non déterminisme.
  • Suppression d’une assertion de l’intérieur d’une boucle.
  • Modification de la représentation des données.

Affichage du Devoir2

03 avr. 2007 
14    Étude de cas :
  • La justification d'un texte à droite.
  • La plus longue séquence croissante.
 10 avr. 2007 
15   
  • Examen final.
  • Remise du Devoir 2.
17 avr. 2007 
6. Évaluation du cours :

L'évaluation est l'appréciation du niveau d'apprentissage atteint par l'étudiant par rapport aux objectifs des cours et des programmes.

L'attribution des notes se fera selon la répartition suivante :
  • Examen de mi-session 30%
  • Examen final 40%
  • Quizs 15%
  • Devoirs 15%
7. Politiques départementales et institutionnelles :
8. Principales références :
  1. Roland Backhousse, Program construction, Calculating implementations from specifications, John Wiley & Sons, 2003.
  2. Ivan Bratko, Prolog, Programming for Artificial Intelligence, third edition, Pearson Education, 2001.
  3. David Gries, The Science of Programming, Springer -Verlag, 1981.
  4. Richard Lassaigne & Michel de Rougemont, Logique et fondements de l'informatique, Hermès, 1993.

La page web du cours se trouve sur WebCT.

9. Page Web du cours :