Département d'Informatique

Maîtrise d'Informatique 2001/2002

Spécifications formelles, preuves

& construction de programmes

Travaux dirigés

Mercredi 17 octobre

De l'importance de la notion de type

Où l'on montre que la construction ou la preuve d'un programme sont très liées à la définition des types.

Pour chacune des phrases CAML suivantes, vérifier si les phrases sont bien typées et préciser le type de chaque variable:

let carré x = x*.x;;
let derivée_en (x0,f) = let epsilon = 0.001 in (f(x0+.epsilon)-.f(x0)) /. epsilon;;
let prime f = function x -> derivée_en (x,f);;
prime carré;;

let rec quotient_reste (a,b) = if a < b then (0,a) else 1 + quotient_reste (a-b,b);;

Utiliser le filtrage et le langage CAML pour définir les fonctions suivantes:
1. it_list f a [b1;b2;...;bn] = f (... (f (f a b1) b2) ...) bn
2. list_it f [a1;a2;...;an] b = f a1 (f a2 (... (f an b) ...))
3. combine ([a1;a2;...;an],[b1;b2;...;bn]) = [(a1,b1);(a2,b2);...;(an,bn)]
Comparer les approches CAML et LISP en essayant de définir les fonctions suivantes:
1. Concaténation de 2 listes,
2. Mise à plat d'une liste.
3. Tri d'une liste par insertion.

Comparer les approches CAML et LISP sur le problème de la recherche d'un nombre dans un arbre binaire ordonné de nombres. Exemple d'un tel arbre:

This document was translated from L^AT_EX by H^EV^EA.