L'unité d'enseignement « Fondements de la programmation » est une UE de niveau (300) spécialisation relevant de la licence d'informatique. Elle possède un volume de 6 ECTS et s'étend sur 12 semaines. Elle est placée sous la responsabilité de POUZET, marc.

Description

L'objectif de ce cours est de présenter les fondements de la programmation en initiant les étudiants au raisonnement sur des programmes fonctionnels ou impératifs écrits dans un langage à sémantique sûre. Le langage support de ce cours sera Objective Caml.

Ce cours est composé de trois parties principales: la première partie sera consacrée à la présentation du langage de programmation servant à l'étude et nous choisirons ici Objective Caml; la deuxième partie présente les principes de l'évaluation et du typage des langages de programmation (appel par valeur, appel par nom, évaluation paresseuse; systèmes de types simples, polymorphisme); la troisième partie est dédiée à l'induction et au raisonnement sur les programmes. Elle fera largement appel aux principes de récurrence.

La présentation du langage pourra être réduite si une part significative des étudiants du module a suivi le module "Types et structures de données'' utilisant déjà Ocaml comme langage support.

De même, l'introduction à l'induction pourra être réduite si une part significative des étudiants du module a suivi le module "Structures discrètes".

Préalables et buts pédagogiques

Bibliographie

• Thérèse Accart Hardin, Véronique Donzeau-Gouge Viguié. Concepts et outils de programmation. InterEditions.

• Guy Cousineau et Michel Mauny. Approche fonctionnelle de la programmation. Dunod, 1995.

• Xavier Leroy. The Objective Caml system : documentation and user's manual. 2003.

Contenu indicatif par semaine

1. Présentation du langage Objective Caml. Expressions et valeurs, fonctions, récursivité, modules, bibliothèques, documentation

2. Listes, filtrage, types produits, types enregistrements, sommes, types inductifs (récursifs)

3. Exemples complets, interaction avec le fichier (la compilation vue de l'extérieur)

4. Mécanismes d'évaluation; calculs, valeur, environnement d'évaluation, portée, masquage de noms

5. Liaison statique/dynamique, règles d'évaluation de la partie fonctionnelle (fermetures)

6. Appel par valeur/appel par nom, comparaison avec d'autres langages, traits impératifs

7. Principes du typage (vérification et synthèse automatique): fonctions, applications, récursion

8. Types de données, traits impératifs, polymorphisme

9. Induction et raisonnement sur les programmes (4 cours). Récurrence sur les entiers, ensembles inductifs, équivalence de programmes sur les entiers

10. Types inductifs, renforcement d'une propriété (invariant), pré et post-condition

11. Propriétés de programmes, terminaison

12. Raisonnement sur les programmes impératifs (boucles while, tri, arrêt)