Text preview for : programmation.pdf part of Jean goubault Programmation Livre de programmation en pdf et en français.
Back to : programmation.pdf | Home
Programmation
Jean Goubault-Larrecq LSV/CNRS UMR 8643 & INRIA Futurs projet SECSI & ENS Cachan 61 avenue du pr´ sident-Wilson, F-94235 Cachan Cedex e [email protected] Phone: +33-1 47 40 75 68 Fax: +33-1 47 40 75 21 21 novembre 2003
R´ sum´ e e Ce document sert de notes de cours pour le premier quart du cours de programmation du ´ magist` re STIC, ENS Cachan, edition 20032004. Il s'agit de la version 1, qui date du 02 e octobre 2003 (lecon 1), du 16 octobre 2003 (lecon 2), du 20 octobre 2003 (lecon 3), du 23 ¸ ¸ ¸ octobre 2003 (lecon 4). ¸
Table des mati` res e
1 Lecon 1 ¸ 1.1 Une br` ve introduction aux langages de programmation e 1.2 Quelques bases de th´ orie de l'ordre . . . . . . . . . . e 1.2.1 Points fixes et boucles . . . . . . . . . . . . . 1.2.2 Treillis complets et th´ or` me de Tarski . . . . e e 1.2.3 Cpos, fonctions Scott-continues . . . . . . . . 2 Lecon 2 ¸ 2.1 Langages imp´ ratifs, le langage C . . . . . e 2.1.1 Affectations . . . . . . . . . . . . . 2.1.2 Tableaux, structures . . . . . . . . 2.1.3 Structures de contr^ le . . . . . . . o 2.2 Langages fonctionnels, le cas de mini-Caml . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 3 10 10 13 15 19 19 19 21 24 27
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
3 Lecon 3 ¸ 32 3.1 Architecture et assembleur . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 3.1.1 M´ moires . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 e 3.1.2 Le processeur . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 1
4 Lecon 4 ¸ 4.1 S´ mantique d´ notationnelle de mini-Caml . . . . . . e e 4.1.1 Quel genre de cpo nous faut-il ? . . . . . . . 4.1.2 S´ mantique d´ notationnelle des expressions . e e 4.1.3 S´ mantique d´ notationnelle des programmes e e
5 Lecon 5 ¸ 5.1 S´ mantique op´ rationnelle grands pas de mini-Caml . . . . . . . . . e e 5.1.1 Cl^ tures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . o 5.1.2 Appel gauche-droite, par valeur, par n´ cessit´ , par r´ f´ rence . e e ee 5.1.3 Autres r` gles . . . . . . . . . . . . . . . . . . . . . . . . . . e 5.1.4 S´ mantique op´ rationnelle des programmes . . . . . . . . . . e e 5.1.5 Arbres de d´ rivations, r´ currence sur les d´ rivations . . . . . e e e 5.1.6 R` gles d´ riv´ es . . . . . . . . . . . . . . . . . . . . . . . . . e e e ` 5.1.7 Correction de la s´ mantique concr` te par rapport a l'abstraite . e e A Guide de r´erence rapide de l'assembleur Pentium ef´
¡ ¢
3.2
3.1.3 Modes d'adressage et formats d'instructions . 3.1.4 Formalisation . . . . . . . . . . . . . . . . . La s´ mantique d´ notationnelle (de mini-Caml) . . . e e de Plotkin . . . . . 3.2.1 Domaines, le mod` le e
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
39 42 46 47 52 52 52 55 58 60 60 60 63 64 65 66 69 72 76
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
2
1
Lec on 1 ¸
1.1 Une br` ve introduction aux langages de programmation e
Il existe de nombreux langages de programmation. En fait, en comptant les langages d'usage g´ n´ ral, les langages de script, les langages d´ di´ s a une application, ..., le nombre de langages e e e e ` existants se compte en dizaines de milliers. Aujourd'hui, les langages les plus couramment r´ pandus sont C, C++ et Java. Il s'agit de e langages imp´ ratifs, c'est-` -dire o` l'ex´ cution proc` de par changements d'´ tats successifs. Par e a u e e e exemple, la factorielle (un exemple que je reprendrai jusqu'` la naus´ e dans la suite de ce cours) a e s'´ crit en C : e int fact (int n) { int resultat; int i; resultat = 1; for (i=1; i<=n; i++) resultat = resultat * i; return resultat; } ` e ce qui se lit informellement : "pour calculer la factorielle de , mettre le r´ sultat a , puis le multiplier successivement par , par , ..., par ". ` A l'oppos´ , les langages d´ claratifs tentent de d´ crire ce qu'on souhaite calculer sans d´ crire e e e e ^ comment -- ou, sans etre aussi extr´ miste, insistent sur le quoi au d´ triment du comment. Par e e exemple, la factorielle en un langage fonctionnel comme CaML s'´ crira : e let rec fact n = if n=0 then 1 else n * fact (n-1);; ` ce qui correspond bien a la notation math´ matique d´ finissant la factorielle : e e
Un autre exemple est donn´ par les langages logiques, dont le repr´ sentant typique est Prolog, e e ´ o` l'on ecrirait typiquement : u fact(0,1). fact(N+1,Y) :- fact(N,Z), Y=(N+1)*Z.
3
¥ ¨ © ¥
si si
¡
¨
£
¨
¡
§
¢
¥ £ ¦¤
¡
(J'ai en r´ alit´ un peu trich´ dans l'´ criture de ce programme, pour des raisons de lisibilit´ .) Ceci e e e e e d´ finit une relation fact entre deux entiers, telle que fact e est cens´ etre vrai si e^ , , et s'il existe tel que . et d´ finie par le fait que e Je n'insisterai pas sur les langages logiques, que vous comprendrez mieux de toute fac on apr` s ¸ e avoir suivi le cours de logique d'Hubert Comon. ` Le but de ce cours n'est pas sp´ cifiquement de vous apprendre a programmer dans tel ou e ` tel langage de programmation, mais de vous apprendre quelques concepts de base communs a pratiquement tous les langages de programmation. Un concept central est celui de s´ mantique. Plut^ t que de dire de quoi il s'agit tout de suite, e o examinons les questions suivantes : ´ Je vous donne un programme, par exemple le programme fact ecrit en C ou en CaML comme ci-dessus. Que fait ce programme ? Vous pouvez vous laisser guider par une intuition plus ou moins vague de ce que fait chaque instruction du programme. Mais ceci ne m` ne pas toujours loin. Par exemple, sachant que, e en C, ++ ajoute un au contenu de la variable et retourne la valeur qu'avait avant, que fait l'instruction suivante ? x = x++; ` Vous pouvez tester ce programme, et par exemple sur ma machine, ceci ajoute juste a x. Il est probable que, si vous avez un compilateur C qui fonctionne comme le mien, vous soyez convaincus que c'est effectivement ce que doit faire cette instruction. (J'expliquerai la notion de compilateur un peu plus loin.) Mais un jour vous le ferez peut-^ tre tourner sur e une autre machine, ou avec un autre compilateur, et l'instruction ci-dessus ne changera pas ` la valeur de x. La raison en est que x = x++; demande essentiellement a effectuer trois op´ rations : e 2. r´ inscrire e
dans la variable x (l'effet de x++) ;
3. mettre
(la valeur de x++) dans x.
Or les deux derni` res entrent en conflit : on n'obtient pas le m^ me r´ sultat selon qu'on e e e ex´ cute 1 avant 2 ou 2 avant 1, et la norme du langage C ne pr´ cise aucun ordre entre e e ces actions. Plus surprenant, il n'est pas exclu qu'un compilateur d´ cide de traduire cette e instruction sous forme d'instructions assembleur qui mettent essentiellement n'importe quoi dans x. Savoir exactement les effets possibles d'une instruction donn´ e, c'est en conna^tre la s´ mantique. e i e ´ ^ J'ai ecrit deux versions de la factorielle, en C et en CaML, ci-dessus. Comment puis-je etre s^ r qu'ils calculent la m^ me chose ? u e ´ Evidemment, j'ai tout fait pour, donc ils devraient calculer la m^ me chose... mais j'ai pu e me tromper (il peut y avoir des bogues). Comment sais-je que je ne me suis pas tromp´ , ou e comment puis-je trouver les bogues ? Il y a plusieurs approches : utiliser un d´ bogueur, ou e effectuer des campagnes de tests, permettent de d´ tecter ou de comprendre des erreurs, du e moins si ces erreurs se manifestent suffisamment fr´ quemment et de fac on suffisamment e ¸ reproductible.
4
1. lire la valeur de x avant, appelons-la
;
¤¥ £ ¡ ©
¡
¨ ¦
¥
¥
£
¦
¥
£¡ ¢
£
¡
¨ ©§ ¦
¥
¥
£
¨
¥
¡
¡
¨
On peut aussi tenter de d´ montrer un th´ or` me d'´ quivalence des deux programmes. Ceci e e e e ` e revient a d´ montrer que les deux programmes ont la m^ me s´ mantique, ou dans les cas e e plus complexes, ont des s´ mantiques reli´ es par des relations ayant de bonnes propri´ t´ s e e ee (relations d'abstraction, de raffinement, bisimulations ; ce ne sera pas le programme de ce cours). Pour ceci, on aura besoin de d´ finir math´ matiquement les diverses s´ mantiques de nos e e e langages de programmation. J'ai parl´ un peu plus haut de compilateurs (vers le langage assembleur). Un compilateur e est un programme, qui prend le texte source d'un programme en entr´ e (par exemple en e C ou en CaML), et le traduit en un autre langage (typiquement le langage machine, ou assembleur). Une s´ mantique, c'est fondamentalement pareil : c'est une fonction prenant e en entr´ e un texte source et retournant un objet math´ matique. e e ` Si l'on arrive a consid´ rer les programmes (C, CaML, assembleur) comme des objets e math´ matiques, les compilateurs ne seront rien d'autre que des fonctions de s´ mantique e e particuli` res. L'avantage de cette vision sera en particulier que l'on pourra d´ montrer qu'un e e ` ` compilateur est correct par rapport a une s´ mantique : ceci reviendra a montrer que deux e ´ ´ s´ mantiques sont equivalentes (typiquement, que ce sont deux fonctions egales). e ´ Ce cours abordera donc des extr^ mes assez eloign´ s : e e D'un c^ t´ nous aurons un peu de math´ matiques : s´ mantiques d´ notationnelles, op´ rationnelles ; oe e e e e th´ orie de l'ordre et th´ or` mes de points fixes, th´ orie de la d´ monstration et r´ currences e e e e e e structurelles. ` De l'autre nous aurons a voir quelques consid´ rations tr` s pratiques : pour comprendre e e la s´ mantique de l'assembleur, il faudra comprendre comment fonctionne un ordinateur : e processeur, m´ moire, bus, portes logiques et flip-flops. C'est l'architecture des ordinateurs, e ` a laquelle B´ atrice B´ rard vous donnera une introduction en deux s´ ances de quatre heures. e e e ` Avant de passer a la suite, consid´ rez le programme suivant en C, si vous comprenez d´ j` le e ea C (on d´ cortiquera ce programme en cours) : e
5
while (n1-- !=0) *res++ = *l1++ ; while (n2-- !=0) *res++ = *l2++ ;
void sort (int *l, int n) int *aux = (int *) malloc (n * sizeof (int)) ; sort1 (l, n, aux) ; free (aux) ; Il s'agit d'un programme de tri d'un tableau l d'entiers, de longueur n, par la m´ thode dite e de tri par fusion. Ce programme contient un gros bogue : lequel ? Vous pouvez le trouver par test et d´ boguage, ou en raisonnant formellement. Dans tous les cas, je ne pense pas que vous e voyiez lequel il est en moins de cinq minutes. Ceci nous m` ne a l'id´ e qu'on aimerait disposer e ` e de m´ thodes automatiques de preuve de programme. Ce sera en particulier le sujet du cours e d'analyse statique, une famille de techniques permettant de d´ tecter certaines propri´ t´ s simples e ee d'un programme, et celui des logiques de Hoare et variantes, qui seront vues plus tard dans ce cours de programmation. Un autre exemple que je prendrai dans ce cours est le petit programme de la figure 1. Tapez-le dans un fichier que vous nommerez cat.c. Il s'agit d'un autre exemple que je r´ utiliserai jusqu'` la naus´ e. Il s'agit du texte source de l'utilitaire cat d'Unix. (Du moins, e a e d'une version na¨ve, mais qui fonctionne.) Ce programme est cens´ s'utiliser en tapant sous le i e shell (interpr` te de commandes Unix), par exemple : e cat a b ce qui va afficher le contenu du fichier de nom a, suivi du contenu du fichier de nom b. (Vous aurez pris soin de cr´ er deux fichiers nomm´ s a et b d'abord, bien s^ r.) En g´ n´ ral, cat suivi e e u e e de noms de fichiers , . . ., , va afficher les contenus des fichiers , . . ., dans l'ordre ; ceci les concat` ne. e Si, au lieu d'utiliser l'utilitaire Unix cat, vous essayez d'utiliser le programme cat.c cidessus, par exemple en tapant : cat.c a b ` vous verrez que cela ne fonctionne pas. C'est parce que le processeur de la machine, c'est- a-dire le circuit int´ gr´ qui fait tous les calculs dans la machine en face de vous (Pentium, PowerPC, ou e e 6
¡
if (n==0) return ; *res = *l ; return ; if (n==1) k = n / 2; sort1 (l, k, res) ; sort1 (l+k, n-k, res+k) ; merge (res, k, res+k, n-k, l) ;
¥ ¦¢
£ §¢
¡
¡
void merge (int *l1, int n1, int *l2, int n2, int *res) while (n1 !=0 && n2 !=0) if (*l1 < *l2) *res++ = *l1++ ; n1-- ; else *res++ = *l2++ ; n2-- ;
void sort1 (int *l, int n, int *res) int k ;
¡
¥ ¦¢
£ ¤¢
¡
¡
¡
#include main (int argc, char *argv[]) { int i, c; for (i=1; i
contrario, le programme cat.c est bien plus lisible, mais le processeur ne le comprend pas. La traduction du fichier cat.c (le source) en cat (l'ex´ cutable) se fait au moyen d'un e compilateur. Par exemple, la commande gcc est le compilateur C, et si l'on tape : gcc -o mycat cat.c le compilateur gcc va traduire (compiler) le source cat.c en un ex´ cutable que j'ai d´ cid´ de e e e nommer mycat, pour ne pas pr^ ter a confusion avec l'utilitaire standard cat. Vous pouvez alors e ` lancer mycat, et v´ rifier qu'il donne bien les r´ sultats attendus en tapant la ligne de commande e e suivante, et en comparant avec ce qui se passait avec le programme cat : ./mycat a b ` ` (Le "./" avant mycat nous sert a dire au shell que l'outil de nom mycat a utiliser est celui qui est dans notre r´ pertoire courant.) e
EXERCISE 1.1
Que se passe-t-il si vous tapez la ligne suivante ? ./mycat cat.c Vous pouvez aussi voir comment fonctionne mycat en utilisant le d´ bogueur ddd : e
EXERCISE 1.2
Sous Unix, avec ddd install´ (sinon, utilisez gdb, mais c'est moins lisible. . .) : e Recompilez mycat en tapant gcc -ggdb -o mycat cat.c. L'option -ggdb permettra au d´ bogueur de vous afficher des informations pertinentes (pour plus d'informae tion, tapez man gcc). Tapez ddd mycat &. La fen^ tre de ddd s'ouvre, montrant le texte source cat.c. Fere mez la fen^ tre "Tip of the Day" si besoin est. e Cliquez sur le d´ but de la ligne int i, c; avec le bouton droit de la souris, d´ roulez le e e ^ menu qui s'affiche, et cliquez sur "set breakpoint". Une petite ic one figurant un panneau stop rouge s'affiche par-dessus la ligne. En plac ant la souris sur la case du bas, o` s'est affich´ le message : ¸ u e (gdb) break cat.c:5 Breakpoint 1 at 0x8048536: file cat.c, line 5. (gdb) tapez run a b. Ceci lance le programme mycat, avec arguments les cha^nes de cai ract` res a et b. Le programme s'arr^ te sit^ t lanc´ sur le "breakpoint" que l'on a mis cie e o e dessus. Tirez le menu "View", et cliquez sur "Data Window" ; cliquez ensuite sur les menus "Data/Display Arguments" et "Data/Display Local Variables". Pour voir les arguments ´e ("a", "b") qui ont et´ pass´ s au programme mycat, cliquez sur le menu "Data/Memory...", e ´ et ecrivez 3 en face de "Examine", puis "string" au lieu de "octal", enfin tapez argv[0] dans la case apr` s "from", puis cliquez sur les boutons "Display" puis "Close". Vous aurez e probablement besoin de r´ organiser le cadre du haut de la fen^ tre de ddd pour bien voir e e les affichages "Args", "Locals" et "X". 8
F IG . 2 Une session sous ddd
9
Cliquez ensuite sur le bouton "Next" de la fen^ tre flottante "DDD" r´ p´ titivement pour e e e ` voir le programme s'ex´ cuter petit a petit. Si vous voulez voir le contenu de la variable c e sous forme d'un caract` re lisible plut^ t que sous forme d'un entier, cliquez avec le bouton e o droit sur la ligne de c dans l'affichage "Locals", tirez le menu local "Display/Others...", ´ ecrivez (char)c dans le cadre sous "Display Expression", puis cliquez sur "Display". ` ^ Vous devriez obtenir quelque chose qui ressemble a la figure 2 ; Vous pouvez bien sur effectuer la m^ me manipulation avec d'autres programmes, y compris ceux de factorielle ou de tri d´ crits e e plus hauts.
1.2 Quelques bases de th´ eorie de l'ordre
Pour vous reposer des aspects pratiques de la section pr´ c´ dente, on va faire ici un peu de e e math´ matiques... math´ matiques qui nous serviront dans la suite. e e 1.2.1 Points fixes et boucles Sans dire tout de suite ce qu'est une s´ mantique, imaginons qu'il s'agit d'une fonction e ` chaque programme associe une valeur qui a dans un certain domaine de valeurs . Un des int´ r^ ts de cette approche, qui s'appelle la s´ mantique d´ notationnelle et qui date de la fin ee e e ´ des ann´ es 1960, c'est qu'en principe on pourra ecrire et prouver des th´ or` mes de la forme : e e e
ou bien
par exemple. ` e L'un des probl` mes centraux a r´ soudre dans une telle approche sera de donner une s´ mantique e e aux boucles. Consid´ rons en effet la boucle while du langage C. Cette construction prend la e forme while (b) e ´ o` b est une expression bool´ enne (retournant vrai ou faux), et e est un bloc d'instructions ecrites u e en C. Une telle boucle fait les op´ rations suivantes : e 1. Calculer b. ` e 2. Si le r´ sultat vaut vrai, alors ex´ cuter les instructions de e, et revenir a l'´ tape 1. e e 3. Sinon, sortir de la boucle. Par exemple, la boucle while (n1!=0 && n2!=0) { if (*l1 < *l2) { *res++ = *ll++; n1--; } else { *res++ = *l2++; n2--; } } 10
¤ ¦¢
£
¢
("les programmes
et
ne font pas la m^ me chose") e
¤ ¥¢
£
¢
("les programmes
et
font la m^ me chose") e
¡
£
¢ ¡
¡
¢
¤ ¥¢
¡ ¤ ¥¢
¥
¡
£
¥
¢
¡
£
¢
de la fonction merge teste si n1 et n2 sont tous les deux non nuls ; si c'est le cas, les trois lignes suivantes sont ex´ cut´ es, puis l'on revient au d´ but de la boucle ; sinon, la boucle est termin´ e. e e e e Un autre exemple est donn´ par la boucle e while ((c = fgetc (f))!=EOF) fputc (c, stdout); du programme cat.c. La condition bool´ enne b est (c = fgetc (f))!=EOF, qui lit le cae ract` re suivant dans le fichier f par fgetc (f), le stocke dans la variable c (c = fgetc (f)), e puis retourne vrai si et seulement si ce caract` re est diff´ rent du marqueur de fin de fichier EOF. e e ` ` Si ce test r´ ussit, autrement dit si l'on n'est pas encore a la fin du fichier f, l'instruction e, a e savoir fputc (c, stdout);, est ex´ cut´ e : elle affiche le caract` re c sur le fichier stdout e e e ´ (la sortie standard), c'est-` -dire (en g´ n´ ral) sur votre ecran. a e e Maintenant, il semble intuitif que while (b) e devrait faire la m^ me chose que le proe gramme if (b) { e; while (b) e } qui teste d'abord si b est vrai, et si c'est le cas ex´ cute e puis la boucle proprement dite. (On e dit qu'on a d´ roul´ la boucle un coup.) Ceci se manifeste par le fait que l'on souhaiterait que e e l'´ quation suivante soit vraie : e
Notons l'inconnue . Il est intuitivement naturel de penser que ceci signifie que ` et if (b) { e; } devraient avoir la m^ me s´ mantique. Si l'on note la fonction qui a e e tout programme associe if (b) { e; }, on voit que nous cherchons sous la forme d'un point fixe de : et doivent avoir la m^ me s´ mantique. e e
´ Cet argument n'est pas tr` rigoureux. Plus formellement, etendons la syntaxe des programmes de sorte qu'ils es puissent contenir des param` tres e , . . ., d´ enotant des programmes non encore explicit´ Appelons es. ´ contexte tout -uplet de valeurs (´ements de ). On peut imaginer etendre la fonction de el´ ` ` etres, et un contexte , et retours´ emantique a une fonction prenant un programme a param` nant une valeur , d´ enotant intuitivement la valeur du programme lorsque vaut , . . ., vaut . (Cette intuition se formalise par l'´ equation ` o` d´ u enote la substitution.) Supposons pour simplifier. Soit la fonction qui a associe ` . Le d´ eroulement de boucle revient a demander que , ce qui est l'´ enonc´ e pr´ du fait que est un point fixe. ecis
$ %! " #! ©
Un autre exemple o` l'on aura besoin de la notion de point fixe est dans la d´ finition de u e fonctions r´ cursives. Consid´ rons le calcul de factorielle 7 en Caml : e e let rec fact n = if n=0 then 1 else n * fact (n-1) in fact 7;; 11
@h $ P igfC%eS3Bdc¥#! aGYXVBUGTS3DIRQIHCG9 b $ ! 1 2 2 2 1 " P b " ` A 9 W 6 @ $ P 9 1 2 2 2 1 @ " P 9 ' @ A
" F(
8 s ut(
6 $ ( 1 2 2 2 1 " ( 754333B0)'
" E!
6 ' r §)a W
A
¡
¡
,
¨ r
©
¨ ¦ ¤ ¢ £§¥£¨ 8 &
A
©
q cp& W
¤
¥
¡¨
¡¨
©
6 $ ( 1 2 2 2 1 " ( 754330)'
6 $ ( 1 2 2 2 1 " ( ' @ A 754333B0)DC9
¨ ¦ ¤ ¢ £§¥£¡
¨ ¦ ¤ ¢ £§¥
6 ( ' @ " ! 6 ' w v )D¥TTyx¡9
&
@ 9
$ 5(
b
$ %!
On voit que fact est une fonction qui est d´ finie en termes d'elle-m^ me : la d´ finition de fact, e e e ` ` apr` s le premier signe =, fait appel a fact (que l'on applique a n-1). (Le fait que fact soit e d´ finie en termes d'elle-m^ me est la raison d'^ tre du mot-cl´ rec, qui instruit le compilateur e e e e Caml de ce fait.) C'est peut-^ tre un peu plus clair si l'on r´ ecrit l'expression Caml ci-dessus en : e e´ let rec fact = fun n -> if n=0 then 1 else n * fact (n-1) in fact 7;; ` o` la construction fun n -> [...] d´ note la fonction qui a n associe [...]. Remplac ons fact par u e ¸ e l'inconnue dans sa d´ finition, et soit la fonction qui au programme associe le programme fun n -> if n=0 then 1 else n *
(n-1)
´ On a donc d´ fini fact comme etant un point fixe de . e ´ Les deux exemples des boucles while et des fonctions r´ cursives ne sont pas si eloign´ s e e qu'il y para^t. La boucle while (b) e peut en effet se coder en CaML sous la forme : i let rec boucle () = if (b) then (e; boucle ()) else () in boucle ();; Rappelez-vous comment on calcule le point fixe d'une fonction contractante de dans : partant de n'importe quel point , on calcule les it´ r´ s ee (o` u , ), et la limite est l'unique point fixe de . Nous ne pourrons pas supposer que nous ` sommes dans un espace m´ trique complet dans la suite, ni que la fonction qui a un programme e associe if (b) { e; } est contractante, mais nous tenterons de calculer la s´ mantique e de la boucle comme une sorte de limite des it´ r´ s ee pour une certaine valeur . Observons ` que cela revient a dire que la s´ mantique de while (b) e est la "limite" de e
^ ` Le probl` me de base va etre de trouver des cat´ gories de domaines de valeurs ou toute fonce e tion (raisonnable) aura au moins un point fixe. 12
¥
¡
£ ¢¥ ¡
¥
¡
¡ ¡ ¤¤¡
¥
¨
¡ ¤¡
¨
©
¡
¤d¨ ©
¥
¨
¤d¨ ©
©
¤
¤d¨ ©
¤
©
¤
¥
e
1.2.2 Treillis complets et th´ eme de Tarski eor` L'une des cat´ gories les plus simples o` l'on aura un th´ or` me du point fixe est celle des e u e e treillis complets et des fonctions monotones. est une relation binaire r´ flexive e Rappelons qu'une relation d'ordre sur un ensemble ( ), antisym´ trique ( e et impliquent ), et transitive ( et impliquent ). Un ensemble ordonn´ est un couple e form´ d'un ensemble et d'une e relation d'ordre sur . On notera souvent au lieu de , par abus de langage. Une fonction sera dite monotone si et seulement si elle pr´ serve l'ordre : si e , alors . ´e ´ ` est un el´ ment sup´ rieur ou egal a e Rappelons aussi qu'un majorant d'une partie de ´e ´ ` ´e tout el´ ment de : pour tout . Un minorant est inf´ rieur ou egal a tout el´ ment e pour tout . La borne sup´ rieure de est le plus petit des majorants de e de : dans , si elle existe ; elle est alors n´ cessairement unique. De m^ me, la borne inf´ rieure de e e e est le plus grand des minorants de dans , si elle existe ; elle est alors n´ cessairement unique. e
¢
´e Si , est par d´ finition le plus grand el´ ment de , et sera not´ ; e e est le plus ´e petit el´ ment de , et sera not´ . On notera aussi e la borne sup´ rieure de la famille e , et de m^ me e sa borne inf´ rieure. On notera aussi e et . Pour faire court, on dira aussi "le sup" au lieu de "la borne sup´ rieure", et "l'inf" pour e "la borne inf´ rieure". e Un inf-demi-treillis complet est un ensemble ordonn´ e non vide tel que toute famille a une borne inf´ rieure e . Montrer que toute famille a une borne sup´ rieure e , et que donc tout inf-demi-treillis complet est un treillis complet. (Indication : s'il existe est le plus petit des majorants... comment peut-on donc le construire ?)
EXERCISE 1.4
Montrer que tout sup-demi-treillis complet (notion que vous d´ finirez par analogie avec la e pr´ c´ dente) est un treillis complet. e e
¢
Par l'exercice 1.4, l'ensemble des ouverts d'un espace topologique est un treillis complet : le sup d'une famille d'ouverts est juste leur union. Quel est son inf ? Le point important est que toute fonction monotone d'un treillis complet dans lui-m^ me a un e point fixe :
¢
13
EXERCISE 1.6
Soit un ensemble quelconque, treillis complet.
l'ensemble de ses parties. Montrer que
0 US
WV ¡
V
TS
EXERCISE 1.5
3
¡ 0 1¥
EXERCISE 1.3
est un
¥
¢
D´ efinition 1 (Treillis complet) Un treillis complet est un ensemble ordonn´ e que toute famille a une borne sup´ rieure e et une borne inf´ rieure e
! ¡ © ¤ ¨¤ ¥¢
.
¤QPG ¡ I¤ 3 523 6 4 ) ¡
¥
¤ F HG
¡ ¡ ¤§¥ ¡
¢
¡
¡
B8 8 )A@93
¢
¤
¢
¡
3
¡
¡
¡ % ## ¤
¤ ¦¤ ¥£
7
4
¡ ¡(' % &¤ ¡ ¤ $ # ¡ " ¢ ¢ ¡ ¢ ¡ © ¨ ¢ B8 8 CE@D4
¡ 0 21
¥
¡
5 5 (4 1¥
¡
¡ R 4 ¤ B CA@8 8
3 ¡ 0 1¥
S
¢
non vide tel
Th´ eme 1 (Tarski-Knaster) Soit eor` un treillis complet. Soit une fonction monotone. Alors a un plus petit point fixe et un plus grand point fixe . De plus de tous les points fixes de , ordonn´ s par , est treillis complet. e l'ensemble Avant d'en faire la d´ monstration, consid´ rons l'intuition donn´ e a la fin de la section 1.2.1. e e e ` Partant de , on va calculer , , . . ., , ... Le sup de cette famille, , v´ rifie : e (pour tout )
donc , mais l'in´ galit´ inverse ne tient pas en g´ n´ ral (voir exere e e e cice 1.10). On pourrait utiliser cette forme d'argument en it´ rant de fac on transfinie, mais ceci e ¸ n´ cessiterait que nous parlions d'ordinaux... et ce n'est pas un cours de th´ orie des ensembles. e e D´ emonstration. Consid´ rons l'ensemble e des post-points fixes de . D'abord remarquons que est non vide, car est dans ; ceci n'a pas en r´ alit´ beaucoup d'importance. e e a une borne inf´ rieure ; appelons-la . Comme e Puisque est un treillis complet, est un minorant de , pour tout . Comme est monotone, ´ , et comme , : donc . Ceci etant vrai pour tout , est un minorant de . Comme est le plus grand de tous ces minorants, . Mais ceci, par d´ finition, signifie que e est dans , et est donc le plus petit post-point fixe de . Revenons sur le fait que . Par monotonie de encore, , donc est aussi un post-point fixe de . Comme est le plus petit, . Donc par antisym´ trie. Ceci montre que est un point fixe de . e C'est n´ cessairement le plus petit de tous les points fixes : tout autre point fixe de est e ´ clairement un post-point fixe de , et est donc sup´ rieur ou egal au plus petit post-point fixe . e La fin de la d´ monstration est laiss´ e en exercice. e e
EXERCISE 1.7
Terminez la d´ monstration du th´ or` me de Knaster-Tarski. (Attention : le sup dans d'une fae e e mille de points fixes de n'est pas n´ cessairement un point fixe de , et il faudra donc construire e le sup dans d'une famille de points fixes de l´ g` rement diff´ remment ; indication : e e e pensez post-points fixes...)
EXERCISE 1.8
D´ montrez le th´ or` me de Cantor-Schr¨ der-Bernstein en utilisant le th´ or` me de Knastere e e o e e Tarski : si est une injection de dans et une injection de dans , alors il existe une bijection entre et . Indication : trouvez une partie de v´ rifiant certaines propri´ t´ s sugg´ r´ es e ee ee par la figure ci-dessous, en vous souvenant que est un treillis complet (exercice 1.5).
14
%
$%
¡
7 ¥ ¢ ¨§@ ¥ 3
¡
¢
¢
¤¢
¡
¥
¤¢
¢ £¢ ¤ ¢
¡
¡ ¡
¢ #"¢
¡
¢ ¢ ¢
¡
¢
S
¢
¢ ¢
¢!
¢
6 ¡ % ¨¨
¢
&
¢
¢ ¢
¢
¥
0 TS S ¡
¢
¢
¢ ¢
¢
7 ¥ ¢
7 £ ¢¥ ¢ ¡ 7 ¥ ¢ ¢
% &
¢ ¢ £¢ ¢
¡
¤
¢ ¢
¢ "¢
¢ "¢
¡
¢
¥
7 ¤ ¢ 7
&
¢
7 ¥ ¢ ¨§@ ¥ 3
§ 7 ¥ ¢ @ © ¥
¢
¢
S
¢
¢ "¢ ¢ #"¢
¢
¢
¢
%
¢
¢ ¢
7 ¥ ¢ @ ¥ 3 ¤¢ §
¢
&
¥ ¦
¥ ¦
¡
7
¢
S
¢
¢
¢ "¢
¢ ¢
¢
A
B
g
X
f
` une fonction monotone, au sens ou et impliquent ` . Par le th´ or` me de Knaster-Tarski, e e existe pour tout , ou ` ` d´ note la fonction monotone qui a associe e . Montrer que la fonction qui a associe est monotone de dans . (Indication : utiliser la caract´ risation du plus petit e point fixe comme plus petit post-point fixe.) Soit l'intervalle de la droite r´ elle, muni de son ordre naturel . Montrer que e est un treillis complet. Si est une fonction monotone de dans , montrer que ` pour toute suite croissante si et seulement si est continue a gauche sur . En choisissant judicieusement , en d´ duire que e est en g´ n´ ral diff´ rent e e e de . 1.2.3 Cpos, fonctions Scott-continues Historiquement, Dana Scott avait propos´ d'utiliser les treillis complets comme domaines e ` de valeurs servant a donner des s´ mantiques aux langages de programmation. Une notion e importante d´ couverte par D. Scott est que toutes les fonctions calculables de dans sont non e seulement monotones mais encore continues (au sens de Scott, voir plus loin). Plus tard, d'autres, et notamment Gordon Plotkin, se sont aperc us que l'on pouvait se passer de treillis complets, et ¸ utiliser des ensembles ordonn´ s plus g´ n´ raux : les cpos ("complete partial order"). e e e D´ efinition 2 (Famille dirig´ fonctions Scott-continues) Soit ee, un ensemble ordonn´ . Une e famille est dite dirig´ e si et seulement si : e est non vide ; et pour tous dans , et ont un majorant dans . Une fonction est Scott-continue si et seulement si, pour toute famille dirig´ e qui e a un sup , la famille a un sup et .
15
¥
¥
¡
£
§ ¨ ¥
@ 3
£
¢
£
¡
7
¢
¢
¥
¢ ¨ ¥ §
¡
@ 3
£
£
¢
¢
¡
3
¥
£
§ ¨ ¥ ¥
@
3
¢
¡
¢
¤
£
£ ¤¢
¤£¡ ¨ ¢
EXERCISE 1.10
¢
¤
¢
¤
¤
¢
¤¤¢
¢ £¢
¡
Soit
¢
¤ ¤
¢
¤
¢
¡
¥
¤ ¢ ¤ ¢ ¡ ¡ ¡ § ¢
¥
EXERCISE 1.9
¥
¢
¢
¡ &¢ R¤
¢
¢
¡ 20
7 ¥ ¢ ¨§@ ¥ 3
£
£
¥
3
¢
£
¤
£
¡ ¢ ¥ §
¡
¢ £¢ ¢
¢
¤£@ ¨ ¢3
¡
Cette d´ finition est une g´ n´ ralisation, qui s'est av´ r´ e naturelle, de ce que nous voulons vraie e e ee ment repr´ senter. Reprenons la construction du plus petit point fixe sous forme de e , ´ est dirig´ e, d'abord : c'est e construction qui avait echou´ en section 1.2.2. La famille e facile, et c'est le contenu de l'exercice 1.11 ci-dessous. Si cette famille a un sup , la e e Scott-continuit´ de est exactement l'hypoth` se suppl´ mentaire dont nous avions besoin pour e montrer que est le plus petit point fixe de : c'est le lemme 2. une suite croissante quelconque dans . Autrement dit, pour Soit tout . Montrer que forme une famille dirig´ e. Si e est une fonction est une suite croissante, et forme donc une famille dirig´ e. e monotone, montrer que
D´ emonstration. C'est un point fixe :
(par Scott-continuit´ ) e
C'est le plus petit : supposons en effet que est un point fixe, et commenc ons par montrer que ¸ ´ pour tout , par r´ currence sur ; c'est evident si e , et par la monotonie de dans le cas r´ current. On en d´ duit que e e , or puisque . Donc . L'intuition derri` re la notion de Scott-continuit´ est qu'un programme calcule une valeur, et e e qu'en particulier une boucle devrait calculer sa valeur en tant que point fixe. La construction du th´ or` me de Knaster-Tarski est non constructive. L'int´ r^ t de la construction du lemme 2 est e e ee que, en identifiant sup et limite, le plus petit point fixe est construit comme une limite d'it´ r´ s ee ` finis de la fonction , ce qui correspond a l'intuition que nous avons donn´ e a la fin de la e ` section 1.2.1 sur la fac on dont on pouvait imaginer calculer des points fixes. ¸ existe toujours dans un treillis complet. Mais, alors que dans un Maintenant, treillis complet, les sups de n'importe quelle famille existent toujours, ici nous n'avons besoin que de sups de familles dirig´ es. e D´ efinition 3 (Cpo) Un ordre partiel complet, ou cpo ("complete partial order") est un ensemble ordonn´ e dans lequel toute famille dirig´ e a un sup. Un cpo point´ est un cpo ayant un e e el´ ment minimal . ´e
¢
Corollaire 3 Toute fonction continue fixe, qui est le sup des , .
d'un cpo point´ e
dans lui-m^ me a un plus petit point e
16
$%
¥
¥
¢ ¨ ¥ §
@ 3
¨
¥
¥
¢ ¥ §
7 ¢ ¨§@ ¥ 3 @ 3 7 ¥ ¢ @ ¥ 3 ¥ §
¢
§ 7 F 7 £ ¢¥ ¢ @ © ¥ ¡
¡
¥
7 ¢ ¨§@ © ¥ ¥ 7 £ ¢¥ ¢ ¨§@ © ¥ ¡ 7 ¥ ¢ ¢ ¨§@ © ¥
% ¢ 7 ¥ ¢
¤
¥
¥
¥
¥
¢
7 ¥ ¢ ¨§@ ¥ 3
7 ¥ ¢ ¨§@ ¥ 3
¡
7 ¥ ¢ ¨§@ © ¥ ¤¢
¢
7
¢
Lemme 2 Soit el´ ment . Si ´e
une fonction Scott-continue de dans , et supposons que existe, c'est le plus petit point fixe de .
a un plus petit
(trivialement)
£ ¢¥ ¡
¢¥
¡
¡ ¡ ¢¢
EXERCISE 1.11
7 ¢ § ¥ 3 ¥ @ 7 ¥ ¢ ¨§@ ¥ 3
§ ¥
@ 7 ¥ ¢
) ¡ ¡
¢
¢
¡
¢ § ¨ ¥ ¥ § ¨ ¥ ¥ ¡
@ 7 @
7 ¥ ¢ ¨§@ ¥ 3
¢
¡
§ ¨ ¥ ¥
¢
¥
@
¢
% ¡£
7 ¥ ¢
7
¥ @ ¥ 3 § ¢ 7 ¥ ¢
On pourra s'interroger sur l'opportunit´ d'appeler une fonction continue lorsqu'elle pr´ serve e e les sups (vus comme limites). Il se trouve qu'il s'agit r´ ellement de la notion de continuit´ usuelle e e vue en topologie g´ n´ rale. e e un ensemble ordonn´ . Soit l'ensemble e D´ efinition et lemme 4 (Topologie de Scott) Soit des parties de telles que : est clos par le haut : pour tout dans , si alors est dans ; et est inaccessible par le bas : pour toute famille dirig´ e de dont le sup existe et est e a . dans , rencontre , c'est-` -dire Alors est une topologie sur , appel´ e la topologie de Scott. Les el´ ments de sont appel´ s e e ´e les ouverts de Scott de . La propri´ t´ d'inaccessibilit´ par le bas dit, dans le cas o` ee e u est une suite croissante , que si le sup (la "limite") des est dans , alors l'un des est dans . Par contrapos´ e, e toute suite croissante hors de a un sup (limite) hors de , ce qui est une fac on de dire que le ¸ e compl´ mentaire de est ferm´ , dans un sens intuitif. e D´ emonstration. D'abord, la partie vide et lui-m^ me sont dans , clairement. e Ensuite, si est une famille (possiblement infinie) d'ouverts de Scott, on pr´ tend que e est un ouvert de Scott : est clairement clos par le haut, et si est une famille dirig´ e dont le sup existe et est dans e , alors est dans un , donc rencontre , ce qui entra^ne que rencontre i Finalement, si et sont deux ouverts de Scott, montrons que leur intersection en est encore un. Clairement est clos par le haut. Pour toute famille dirig´ e e dont le sup existe et telle que est dans , alors est dans et dans , donc il existe deux ´e et . Comme est dirig´ e, e et ont un majorant dans el´ ments , qui est dans parce que et sont clos par le haut. Donc rencontre .
EXERCISE 1.12
Pour tout dans , notons l'ensemble de tous les dans . Montrer que est un ferm´ de Scott. (On rappelle qu'un ferm´ est par d´ finition le compl´ mentaire d'un ouvert, et e e e e non une partie non ouverte.) Soit une fonction monotone de l'ensemble ordonn´ e dans l'ensemble ordonn´ e . D´ montrer que est Scott-continue si et seulement si est continue pour la topologie de Scott, e autrement dit si et seulement si l'image r´ ciproque de tout ouvert de Scott est encore un ouvert de e Scott. (Pour la direction seulement si, on montrera d'abord que l'image d'une famille dirig´ e par e une fonction monotone est dirig´ e. Pour la direction si, plus difficile, on consid´ rera l'ensemble e e , intersection des lorsque parcourt l'ensemble des majorants de , et on d´ montrera e que est un ferm´ tel que e contient .) Dans la suite, on ne dira plus "Scott-continu", mais simplement "continu", l'exercice 1.13 montrant qu'il n'y a en fait aucune ambigu¨t´ . ie
¢
17
¥
£
¢
EXERCISE 1.13
$%
§ ¥ ¥
@
¤
8
¡ ££
¡
V
£
V
£
£
£
¤
£
¡
¤
V
¡
8
¢
£
£
¤
¥
£
£
¡
¢
5 ¥ £¢£ ¡ ¤2 ¡
¢
£
¢
3
£
£
3
¡
£
£
B 8 CA@8 ¥ 8 B)A@8 8 )¥B A@8 ¥
¤
¡ £ ¤ ££ ¡ ¤ ©£ % ¤ ¡ £ £ % ¡ £ 3 ¤ ©¡¨£ ¡ §¦£
¥
e
¤
¤
¡
£
¢
¤
¡
¤
B C@E8 8 ¤
£
¡
£
¢
£
£
B 8 CE@8 ¥
V
¢
£
Montrez que la topologie de Scott sur n'est en g´ n´ ral pas s´ par´ e (ou Hausdorff, ou : e e e e , il existe un ouvert contenant et un ouvert contenant d'intersection pour tous ´e vide), en ce sens que si elle est s´ par´ e, alors tous les el´ ments de e e sont incomparables pour . Montrez en revanche que toute topologie de Scott est , c'est-` -dire que pour tous a , il existe un ouvert de Scott contenant mais pas , ou bien contenant mais pas . (Utilisez l'exercice 1.12.) ´ Etant donn´ un espace topologique e , son pr´ ordre de sp´ cialisation est d´ fini par : e e e dans , si et seulement si, pour tout ouvert contenant , contient . pour tous Montrer qu'il s'agit bien d'un pr´ ordre, c'est-` -dire d'une relation r´ flexive et transitive. Si de e a e plus la topologie est , alors il s'agit d'une relation d'ordre.
EXERCISE 1.16
Montrer que l'ordre de sp´ cialisation (cf. exercice 1.15) de la topologie de Scott d'un ensemble e ` ordonn´ e quelconque est l'ordre lui-m^ me. (Pour l'un des deux sens de l'implication a e ` d´ montrer, pensez a utiliser l'exercice 1.12.) e L'exercice suivant montre en quoi les sups sont une bonne fac on de parler de limites dans les ¸ cpos.
EXERCISE 1.17
On dit que est une limite de la famille dirig´ e dans l'espace topologique si et seulement e si, pour tout ouvert contenant , il existe dans tel que pour tout dans , est dans . Montrer que le sup de s'il existe est une limite de , pour la topologie de Scott. En vous aidant de l'exercice 1.16, montrer que le sup de s'il existe est en fait la plus grande limite de ` ´ . (On rappelle a ceux que cette formulation etonnerait que le th´ or` me d'unicit´ des limites e e e n'est valable que dans les espaces s´ par´ s...) e e
18
©
£
¡
¡
¤ ©
£
£
£
£
EXERCISE 1.15
¤
¥
"
!
¡
EXERCISE 1.14
¤
¡
¢ ¢
WV ¡
" ¢ ¡ ¡
£
V
"
"
¡
¥
¢
¢
£
2
Lec on 2 ¸
2.1 Langages imp´ eratifs, le langage C
Aujourd'hui nous examinons plus en d´ tail les constructions de base d'un langage imp´ ratif e e typique : le langage C, invent´ par Kernighan et Ritchie au d´ but des ann´ es 1970. e e e ` La chose essentielle a retenir est qu'un programme C d´ finit une s´ quence d'instructions e e ´e el´ mentaires, qui sont des affectations : pour simplifier, les affectations sont des instructions de ` la forme variable = expression ;, qui ont pour effet de calculer la valeur de l'expression a ` droite du signe =, et de la ranger ensuite dans la variable a gauche du signe =. L'organisation des ` affectations en s´ quence se fait a l'aide d'une certain nombre de constructions du langage, que e nous verrons en section 2.1.3. Cette pr´ sentation de C n'est pas compl` te, et on pourra consulter e e diff´ rentes ouvrages de r´ f´ r´ nce, par exemple Le langage C, par Kernighan et Ritchie, ou la e eee r´ f´ rence http://diwww.epfl.ch/w3lsp/teaching/coursC/ par exemple. Pour les ee plus courageux, on pourra aussi consulter la norme ISO/IEC 9899-1999 d´ finissant le C dit e "ANSI C" (le C officiel). 2.1.1 Affectations Par exemple, x = 3; a pour effet de mettre l'entier x = y+1;
dans la variable nomm´ e x. Un autre exemple est l'instruction e
qui r´ cup` re l'entier stock´ dans la variable y, lui ajoute , et range le r´ sultat dans la variable x. e e e e Attention ! Le symbole = n'est pas le pr´ dicat d'´ galit´ que l'on rencontre usuellement en e e e en math´ matique serait celle d'une valeur de e math´ matiques. La signification typique de e ´ v´ rit´ , valant vrai si vaut , et faux sinon. Ici, x = 3 ne teste pas du tout si x egale ou e e non. En revanche, il est vrai qu'une fois l'instruction x = 3 ex´ cut´ e, le contenu de la variable e e ` e e e x vaut effectivement . Un moyen de voir a quel point = n'est pas le pr´ dicat d'´ galit´ des math´ matiques est de consid´ rer une instruction telle que : e e x = x+1; qui r´ cup` re l'entier stock´ dans la variable x, lui ajoute , et range le r´ sultat de nouveau dans e e e e x. Donc, par exemple, si x contient l'entier avant d'effectuer x = x+1;, x contiendra apr` s. e ´ ` En particulier, en aucun cas on n'aura x egal a x apr` s ex´ cution de cette instruction. Mais e e ´ bien s^ r la valeur de x apr` s cette instruction egale la valeur de x avant. u e ´e e Cette ambigu¨t´ , qui peut surprendre ceux qui sont habitu´ s aux math´ matiques, a et´ lev´ e ie e e ´ dans d'autres langages imp´ ratifs, comme Pascal, o` l'on ecrirait x := x + 1, en utilisant le e u symbole := pour bien marquer qu'il s'agit d'une affectation et non d'un test d'´ galit´ . e e ´ Si = est l'affectation, le test d'´ galit´ en C est le symbol ==. On ecrira donc : e e 19
¢
¤
¡
¡
¡
¨
¢ £¥
¢
¡
¢
¢
¡ ¢
if (x==3) ... pour tester si x vaut , et non if (x=3) ... ^ qui, dans un langage un peu plus sur que C, serait une erreur, et serait rejet´ par le compilateur. e Mais C l'accepte gaiement. . . le langage C est en fait tr` s permissif : la s´ mantique de C pr´ cise e e e ^ en effet que toute affectation, par exemple x=3, peut aussi etre vue comme une expression, et a pour valeur la valeur de son c^ t´ droit. Ici, la valeur de x=3 est donc , ce qui permet d'´ crire des oe e expressions comme y=x=3;, qui range dans x (x=3), puis retourne le r´ sultat de l'affectation e x=3, c'est-` -dire , et le range dans y : donc y=x=3; range dans x et dans y. a ` La syntaxe des expressions de C est assez riche, et un aperc u (pas tout a fait complet, voir ¸ ` n'importe quel livre d'introduction a C pour l'ensemble complet) est donn´ en figure 3. e x y ma_variable 0 1 2 -1 -2 'a' 'b' 3.1415926536 % & | ^ >> << ~ == && || ! & variables constantes op´ rations arithm´ tiques e e ` op´ rations bit a bit e comparaisons et, ou, non logiques pointeurs, tableaux appel de fonction
F IG . 3 Un aperc u de la syntaxe des expressions de C ¸ On ne d´ crira pas la s´ mantique des diff´ rentes expressions de C. Sur les entiers (qui sont e e e les entiers machines, pas tous les entiers ! sur une architecture de machine 32 bits standard, les entiers sont ceux compris entre et ), ^ calcule l'addition des valeurs de et (modulo sur une architecture 32 bits ; pour etre pr´ cis, la valeur de e sur ces machines vaut l'unique entier compris entre et ` qui est congru a la somme des valeurs de et modulo ); calcule la diff´ rence de e et (modulo de nouveau sur une architecture 32 bits), calcule le produit de et (modulo ), calcule leur quotient et % le reste de la division de par (modulo ). Attention : ne calcule pas le r´ sultat de la division de par , mais sa partie enti` re e e (le quotient, donc). Par exemple, en C donne , pas ; et % calcule le reste, ici . En revanche, on peut aussi calculer en C sur des nombres flottants (abr´ viation de "nombres e ` ´ a virgule flottante", qui d´ note la fac on de les repr senter sur machine), qui sont des approximae ¸ e tions finies de r´ els. Les op´ rations , , et sont alors les addition, soustraction, multiplicae e ` tion et division usuelles, a arrondi pr` s. Par exemple, 2.0 3.0/ donne vraiment 0.66666666666. e ´ On remarquera que les nombres flottants sont ecrits avec un point d´ cimal ; en particulier, 2 et e 2.0 sont deux objets diff´ rents : l'un est un entier machine, l'autre un flottant. e 20
¡ ¤
£
£¢
¨
£
¤ !¢ ¤ ¤ ¡ ¢ ¥ ¡ £ ¢
¤
£
¢
£
¢
¢ $¦$$$# ¢¤¢ ¨ ¨ ¤ £ ¤ £ ¤ "¡ £ ¤ £ ¤¢ ¤ £ ¤ ¢ £ ¤ ¤ ¢ ¤ ¤ ¡ ¢ ¥ £ ¦¢
¢
¢
¥ ¨ ¥ § ¦¥ £¢ ¤ ¡
¦
¤
¡
¢
¨
¦
¢ ©¨ §
¤
£¢
¨
¤ ¦¤ £ ¤ ¦¤ £ ¤ ¦¢
£
¢
¢
¤ ¦¢
¨
¢
¦¡
¥
¤ ¤ ¢ ¤
£
¢
EXERCISE 2.1
Que valent 1-2, 15/7, 15%7, 1+(3*4), (1+3)*4, 1+3*4 en C ? Vous pouvez vous aider ´ du compilateur gcc, en ecrivant un programme de la forme : #include int main () { printf ("La valeur de 1-2 est %d.\n", 1-2); return 0; } L'instruction printf ci-dessus a pour effet d'imprimer la valeur souhait´ e : faire man printf e pour avoir le modus operandi pr´ cis de printf. e Attention : ceci vous donnera la s´ mantique de 1-2 sur votre machine, pour votre compie lateur particulier. N'en concluez pas n´ cessairement que la s´ mantique de C en g´ n´ ral sera e e e e celle que vous aurez observ´ e sur votre machine. Dans les exemples ci-dessus, cependant, les e ` indications de votre machine seront fiables, et g´ n´ ralisables a toute machine (a priori). e e
EXERCISE 2.2
` Que valent (-10)/7, (-10)%7 sur votre machine ? Ceci correspond-il a ce que vous attenpar , a-t-on ? diez ? Si est le quotient et le reste de la division de
EXERCISE 2.3
Que valent 10/(-7), 10%(-7), (-10)/(-7), (-10)%(-7) sur votre machine ? Inf´ reze et % calculent et tels que en la sp´ cification du quotient et du reste sur votre machine : e , . . . et quelles autres propri´ t´ s d´ terminant et de fac on unique ? ee e ¸
EXERCISE 2.4
Il y a aussi toujours des cas pathologiques. Que valent 1/0, (-1)/0, 0/0 sur votre machine ? (Attention, ceci est totalement d´ pendant de votre compilateur et de votre machine : sur e la mienne, le programme est interrompu par un message Floating point exception, alors m^ me qu'il ne s'agit pas de calcul en flottant mais bien en entier.) e
EXERCISE 2.5
` (Si votre machine a des entiers 32 bits en compl´ ment a deux, ce qui est le cas pour toutes e ` les machines de l'ENS a la date d'´ criture de ce document.) Rappelez-vous que le plus petit e entier repr´ sentable en machine est e , et le plus grand est . L'oppos´ du plus petit entier repr´ sentable n'est donc pas repr´ sentable ! En e e e exp´ rimentant avec gcc, comment calcule-t-il l'oppos´ du plus petit entier repr´ sentable ? Que e e e valent (-2 147 483 648)/(-1), (-2 147 483 648)%(-1) ? 2.1.2 Tableaux, structures ´ J'ai un peu menti en section 2.1.1 en disant que les affectations etaient de la forme variable ^ = expression en C. Les c^ t´ s gauches peuvent en fait etre plus g´ n´ raux. oe e e
21
¡
¥
¡
¡ £ ¦ ¥ ¤¥ ¢
£ ¦¢
¨
¡
¥
¡ £ ¢ £¤¢
£
¨¡
¤
¥
¢ ¤ ¤ ¡
¢
¢ ¥ £ ¦¢
¡
£
§
¤
¡
¡ © ¨ §¥ ¢ ¡ £
¢ ¤ ¤ ¡
¨
¢
` C'est notamment le cas avec les tableaux. En C, on peut d´ clarer un tableau, a l'entr´ e d'une e e fonction, par une d´ claration de la forme e int a[50]; ´ ´e ´e ´ par exemple. Ceci d´ clare a comme etant un tableau de e el´ ments, chaque el´ ment etant un entier machine (de type int). Alors que int b d´ clare b comme une variable contenant un e seul entier, a ci-dessus en contient une rang´ e de cinquante. e ` ´e ´ u On peut acc´ der a chaque el´ ment du tableau en ecrivant a[ ], o` est une expression e ´e retournant un entier. L'expression a[0] a pour valeur le premier el´ ment du tableau, a[1] le deuxi` me, . . ., a[49] le cinquanti` me (attention au d´ calage !). Les expressions a[-1], e e e a[50], a[314675], qui intuitivement d´ noteraient des acc` s en-dehors du tableau, n'ont aue e cune s´ mantique : si l'on insiste pour obtenir leur valeur, on obtient en g´ n´ ral n'importe quoi. e e e ´ ´e On peut aussi ecrire des expressions d'acc` s aux el´ ments de tableaux plus compliqu´ s. e e Par exemple, si i est une variable enti` re, a[i] d´ note l'´ l´ ment num´ ro i (qui est donc le e e ee e ` ´e e ee e i i` me). L'int´ r^ t de ceci est que l'on peut acc´ der a un el´ ment variable, dont l'indice est lui` m^ me calcul´ . Voici par exemple un calcul de produit scalaire de vecteurs a trois composantes : e e float produit_scalaire (float a[3], float b[3]) { float resultat; int i; resultat = 0.0; for (i=0; i<3; i++) resultat = resultat + a[i]*b[i]; return resultat; } ` (La boucle for (i=0; i<3; i++) it` re l'instruction qui suit pour i allant de inclus a e exclu.) ´e Pour changer le contenu des el´ ments d'un tableau, l'instruction d'affectation est en fait plus ´ g´ n´ rale que celle que nous avons vue plus haut. On peut donc notamment ecrire e e a[0] = 5.0; ´e pour mettre le flottant 5.0 en premier el´ ment du tableau (sans toucher aux autres). On peut ainsi effectuer une multiplication matricielle comme suit, par exemple : float a[3][3]; /* Multiplication de matrices 3x3, a et b, r´sultat dans c. */ e float b[3][3]; /* A noter que les tableaux bidimensionnels sont juste des tableaux ` trois ´l´ments a e e de tableaux ` trois ´l´ments. */ a e e float c[3][3]; 22
¢
¨
¨
¡
¨
int i,j,k; for (i=0; i<3; i++) for (j=0; j<3; j++) { c[i][j] = 0.0; for (k=0; k<3; k++) c[i][j] = c[i][j] + a[i][k]*b[k][j]; } Les autres structures de donn´ es importantes en C sont les structures, les unions, et les poine teurs. Je ne parlerai pas des pointeurs ici, et je pr´ f` re attendre que vous ayez vu un peu d'aree chitecture des machines au travers du langage machine en lec on 3 d'abord ; les pointeurs ne se ¸ ` comprennent vraiment qu'une fois qu'on sait comment la machine fonctionne vraiment, a un niveau plus bas. Les structures, appel´ es aussi enregistrements ("records") sont essentiellement des -uplets. e Par exemple, on peut d´ finir le type des nombres complexes en C comme e struct complex { float re; float im; }; ´ Ceci d´ finit un nombre complexe comme etant un couple de deux flottants (sa partie r´ elle et sa e e ´ partie imaginaire). Etant donn´ e une variable complexe z, typiquement d´ clar´ e par : e e e struct complex z; ` ´ ` on pourra acc´ der a sa partie r´ elle en ecrivant x.re, et a sa partie imaginaire par x.im. Les e e identificateurs re et im sont appel´ s les champs de la structure z. De m^ me que pour les tae e ` bleaux, on pourra affecter (la valeur d')une expression a chaque champ individuellement. Par exemple, struct complex x, y, z; z.re = x.re + y.re; z.im = x.im + y.im; calcule dans z la somme des deux nombres complexes x et y.
EXERCISE 2.6
´ Ecrire de m^ me la diff´ rence, le produit, et la division de deux nombres complexes. e e ´ Ecrire un programme de multiplication de deux matrices compl´ ter) : e 23
¢ ¢
EXERCISE 2.7
de nombres complexes (` a
struct struct struct int i,
complex a[3][3]; complex b[3][3]; complex c[3][3]; j, k;
for (i=0; ... Les structures C permettent de d´ crire des produits cart´ siens de types. Si , . . ., e e sont a1; . . . an; } est essentiellement un type de des types C, le type struct toto { -uplets d'objets pris dans , . . ., . ` On peut aussi d´ crire quelque chose qui ressemble a des unions de deux types : e union nombre { int i; float x; }; par exemple d´ crit le type union nombre comme consistant en des objets qui sont des ene tiers machine ou bien des flottants. Je vous d´ conseille d'utiliser cette construction avant de bien e ` comprendre ce qu'elle fait vraiment : consultez n'importe quel livre d'introduction a C. Atten` tion, cette construction n'a en fait pas grand-chose a voir avec l'union ensembliste, malgr´ les e apparences. Elle permet d'autre part toute une s´ rie de hacks (et toute une s´ rie de bogues aussi) e e que je ne peux d´ cemment pas vous recommander. e 2.1.3 Structures de contr^ le o Pour organiser les affectations en s´ quence, le langage C, comme la plupart des autres lane ´ gages imp´ ratifs, dispose d'un certain nombre de constructions de base, etendues par des formes e d´ riv´ es (du sucre syntaxique) : e e l'instruction qui ne fait rien ( !) : elle se note ;, ou bien {} ; e la composition s´ quentielle, ou s´ quence : ; ; ex´ cute l'instruction , puis . Par e e exemple, x=3; y=x+1; commence par ranger dans x ; une fois ceci fait, ceci calcule x+1, soit , et le range dans y ; le test, aussi appel´ la conditionnelle : e
commence par calculer la valeur de l'expression e, qui est cens´ e etre un entier machine. e ^ Cet entier repr´ sente une condition bool´ enne (vrai/faux). Si cet entier est non nul (ce e e qui par convention signifie que la condition est vraie), alors est execut´ e, sinon est e ex´ cut´ e. Par exemple, e e if (x==3) printf ("x vaut bien 3.\n"); else printf("Ah, x ne vaut pas 3, tiens.\n"); 24
¤
£
¤
£
if ( )
else
¤
¥
S
£
£ ¦
S
¥
¢
¤
S
£
£
S
¥
S
£
S
¤
` A noter ici que la s´ mantique de x==3 n'est pas exactement de retourner vrai si x contient e l'entier , et faux sinon ; en fait, x==3 retourne l'entier si x vaut , et sinon. D'autres langages imp´ ratifs ont un type sp´ cial (bool en Pascal, par exemple) pour d´ noter les e e e valeurs de v´ rit´ , C non : en C, les bool´ ens sont cod´ s sous forme d'entiers. e e e e La boucle while : while ( ) commence par calculer . Si est vrai (i.e., un entier non nul), alors est ex´ cut´ e. A la e e ` diff´ rence de la conditionnelle if, une fois l'ex´ cutioin de termin´ e, la boucle revient au e e e d´ but, recalcule : si est vrai de nouveau, est reex´ cut´ , et ainsi de suite, jusqu'` temps e e e a ´ e que devienne faux (le cas ech´ ant). ´ On a d´ j` vu en lec on 1 que la boucle etait s´ mantiquement une conditionnelle plus un ea ¸ e point fixe :
Et c'est tout ! On peut calculer tout ce qui est calculable avec ces seules instructions. C propose aussi quelques extensions syntaxiques. Notamment, le bloc {
}
if (x==3) { y = z; if (z==4) printf ("Non seulement x vaut 3 mais z vaut 4.\n"); else printf ("z ne vaut pas 4, mais y vaut z maintenant.\n"); } else printf ("x ne vaut pas 3.\n");
´ On peut aussi eviter d'´ crire la partie else d'un test dans certains cas : if ( ) e else ;. abr´ viation de if ( ) e Une autre construction tr` s fr´ quente est la boucle for : e e
´ ` o` , , sont des expressions (optionnelles : on peut ne rien ecrire a la place de chacune), et u ´ ` une instruction. Ceci est exactement equivalent a
25
while ( ) {
for (
)
}
¥
£
permet de voir n'importe quelle composition d'instructions (grosse) instruction. Ceci permet notamment d'´ crire : e
¤ £
£
¥
¤
¥
while ( )
if ( ) {
while ( )
}
, . . .,
comme si ce n'´ tait qu'une e
¨
¢
¡
£
¢
¤ £
est une
EXERCISE 2.8
R´ ecrire la fonction fact du d´ but de ce cours en terme de boucle while, comme indiqu´ e´ e e ci-dessus. Ceci est-il lisible ?
EXERCISE 2.9
` L'id´ e de la construction for de C est de simuler une boucle pour i variant de a , comme la e do. . . du langage Pascal ou la construction for i= to construction for i= upto ´ ` do . . . done de OCaml, en ecrivant a la place for (i= ; i<= ; i++) . . .. Cependant, en C, il est l´ gal d'´ crire : e e for (i=1; i<=5; i++) { printf ("La valeur de i est %d.\n", i); i = i+1; } Notez que la bizarrerie est que l'on change la valeur de i dans le corps de la boucle une seconde fois, en avant-derni` re ligne. Que fait ce bout de code ? Peut-on faire pareil en OCaml ? e Finalement, en C on a aussi une construction switch. Disons en premi` re approche que le e code : switch ( ) { case constante : ; break; case constante : ; break; ... ; break; case constante : default: ; break; fait la m^ me chose que (o` i est une variable fra^che) : e u i
La construction switch est cens´ e etre plus rapide que la suite de if ci-dessus. Elle ade ^ met aussi quelques variantes, notamment, si l'on omet le mot-cl´ break en fin d'une ligne e case constante , l'ex´ cution de se continuera sur celle de e . C'est une source courante d'erreurs en C, et un des charmes particuliers du langage. 26
£ ¡
8
8
¡
¡¢
int i; i = ; if (i== constante ) ; else if (i== constante ; else if . . . ... else if (i== constante ; else ;
)
)
£
¢
£
¢
¥
£
¤
£
¡
¡
¡¢
¡
¡
¡
¢
¡¥
¤
¥
£
2.2 Langages fonctionnels, le cas de mini-Caml
Il existe aussi en C une notion de proc´ dure que l'on peut appeler pour faire un calcul auxie liaire, et qui une fois le calcul fait retourne un r´ sultat. C'est ce que nous avons d´ j` fait dans le e ea programme fact. Les langages fonctionnels, et notamment Caml et ses variantes (vous connaissez en g´ n´ ral e e tous Objective Caml, aussi appel´ OCaml) sont centr´ s sur cette notion de fonction. Il y a de e e nombreuses bonnes r´ f´ rences sur OCaml, que l'on peut notamment trouver sur la page http: ee //cristal.inria.fr/. ´ Nous allons plus particuli` rement etudier une version r´ duite d'OCaml, que nous nommerons e e `´ mini-Caml dans la suite. Il s'agit au passage du langage dont vous aurez a ecrire un compilateur, puis un syst` me d'inf´ rence de types, en projet. Le typage vous sera enseign´ par Delia Kesner. e e e Dans la suite de ces notes, je consid´ rerai une version non typ´ e. e e ´ -> , L'essentiel d'un langage fonctionnel est que l'on peut y ecrire des fonctions : fun o` u est une expression du langage, est encore une expression du langage, et d´ note la fonction e ` qui a associe . On appellera une telle construction syntaxique fun -> une abstraction. Ceci est (pratiquement) la notion math´ matique de fonction, comme on le verra quand on e ` en donnera la s´ mantique un peu plus loin. Par exemple, fun x -> x+1 est la fonction qui a e . tout entier associe l'entier On a d'autre part une construction, dite d'application : si d´ note une fonction et d´ note e e un argument possible de la fonction, alors d´ note le r´ sultat de l'application de la fonce e ` tion a l'argument . En particulier, (fun x -> x + 1) (3), que l'on peut aussi noter ` (fun x -> x + 1) 3, a bien pour valeur 4. (On peut rajouter des parenth` ses a volont´ e e ´ autour de sous-expressions pour eliminer les ambigu¨t´ s syntaxiques, comme en C d'ailleurs.) ie ` ´ Le sous-langage de mini-Caml ou l'on ne peut ecrire que des variables, des abstractions ´e ´ et des applications s'appelle le -calcul, et a et´ invent´ et etudi´ par Alonzo Church et ses e e ` successeurs a partir des ann´ es 1930. C'est aujourd'hui un outil fondamental en logique et en e informatique th´ orique ; c'est au passage (pub !) le sujet du cours de logique et informatique du e second semestre, en commun avec l'ENS de la rue d'Ulm. ` En OCaml, on a en plus une construction permettant de donner des noms interm´ diaires a e des variables : let = in a pour effet de calculer la valeur de , de lui donner le nom , puis de calculer . Dans , on a le droit de se r´ f´ rer a pour d´ noter la valeur de . Au ee ` e passage, ceci pourrait s'´ crire autrement, sous forme de l'expression (fun e -> ) , ce ´ ` serait equivalent. . . a part que le syst` me de typage de Caml, que vous verrez avec Delia Kesner, e ´ consid` re la forme let d'une fac on un peu sp ciale, et diff´ rente de la forme utilisant fun et e ¸ e e l'application. On retrouve, comme dans les expressions C, toute une famille de constantes et d'op´ rations e permettant de faire des calculs : les constantes enti` res 0, 1, . . ., -1, -2, . . ., les sommes e , les diff´ rences e , les produits , les quotients entiers (ou divisions flottantes) , les mod , . . ., avec essentiellement la m^ me s´ mantique qu'en C. (Nous consid´ rerons e e e restes que ces op´ rations ont r´ ellement la m^ me s´ mantique qu'en C. En OCaml, pour des raisons e e e e ` a techniques, les entiers ne vont que de sur une architecture 32 bits, et l'on calcule modulo , pas .) 27
¦
¨
¦
¤
¦
¦
¡
¢
¦
$¢
¦
¡
¡
¡
¦
¨
¦
¦
¦
¦
¤¢
¦
£
¢
Une diff´ rence importante avec C est que la valeur des variables ne change pas. En C, on e ´ peut toujours changer la valeur d'une variable, disons x, en ecrivant par exemple x=1. Il n'y a aucune instruction permettant de changer la valeur d'une variable en OCaml ou en mini-Caml. Une ^ cons´ quence est que, une fois calcul´ e la valeur d'une variable, on peut etre s^ re qu'elle vaudra e e u toujours la m^ me valeur. Ceci est important pour la lisibilit´ des programmes. Dans un proe e ^ par exemple, on peut etre s^ r que toute r´ f´ rence u ee gramme Caml de la forme let x=3 in ` e a x dans , aussi loin qu'on se trouve dans le source de la d´ claration let x=..., vaudra 3. ´ crire des instructions apparemment similaires : En C, on peut e { int x; x = 3; ... N ... } ^ ` Mais pour etre s^ r que toutes les occurrences de x dans N se r´ f` rent bien a la valeur calcul´ e 3, u ee e il faudra d'abord s'assurer qu'aucune autre instruction n'a pr´ alablement modifi´ la valeur de x. e e Ceci peut se r´ v´ ler tr` s compliqu´ . e e e e Si OCaml et mini-Caml privil´ gient donc un style d'´ criture math´ matique, o` les variables e e e u ne sont pas des cases o` l'on range des valeurs comme en C, mais des noms d´ notant des valeurs u e calcul´ es par ailleurs, les langages de la famille Caml permettent cependant si on le souhaite e d'´ crire des affectations, plus ou moins comme en C. Pour ceci, on utilise la notion de r´ f´ rences. e ee a pour effet d'allouer (de cr´ er) une nouvelle r´ f´ rence, e ee En mini-Caml, l'expression ref c'est-` -dire une nouvelle case m´ moire. Cette case contient initialement la valeur de . On peut a e ´ ensuite relire le contenu d'une case m´ moire (d´ not´ e par , disons) en ecrivant l'expression e e e ! . On peut aussi effectuer une affectation, et := a pour effet de calculer la valeur de , ` ^ a l'int´ rieur de la e qui doit etre une r´ f´ rence , de calculer , et de stocker la valeur de ee r´ f´ rence . ee Par exemple, let x = ref 0 in !x cr´ er une r´ f´ rence contenant l'entier 0, que l'on rep` re par le nom x, puis relit le contenu de e ee e cette r´ f´ rence : le r´ sultat est 0. Essayons une affectation : ee e let x = ref 0 in (x := 3; !x) Ceci cr´ e une r´ f´ rence contenant 0, remplace son contenu par 3, puis lit ce contenu : le r´ sultat e ee e est 3. Un peu plus compliqu´ : e let x = ref 3 in (x := !x+1; !x) 28
¦
¢
¦
¢
¦
¦
¢
¡
¡
¦
¦
letrec boucle = fun () -> if then ( ; boucle ()) else ();; boucle () ` qui d´ finit d'abord un point fixe du if sous forme d'une fonction boucle a un argument (bie don), puis demande la valeur boucle() du point fixe. La construction letrec = ;; sera la seule construction de programme mini-Caml (les constructions vues plus haut sont des constructions d'expressions). Elle d´ finit comme valant e ` exactement la m^ me chose que , et ce m^ me si e e fait appel a . Pour des raisons techniques, ` ^ on restreindra . Une d´ finition via e a etre elle-m^ me la d´ finition d'une fonction e e letrec (par exemple, pour boucle) de est une d´ finition r´ cursive, c'est-` -dire que est e e a ^ d´ finie en fonction d'elle-m^ me. Ceci signifie bien s^ r que doit etre d´ finie comme un point