Concepts et sémantique des langages de programmation 1
constructions fonctionnelles et impératives avec OCaml, Python, C et C++
Thérèse Hardin
Mathieu Jaume
François Pessaux
Véronique Viguié Donzeau-Gouge
Iste éditions
Préface1
Gilles Dowek et Catherine Dubois
Avant-propos3
Chapitre 1. Du matériel au logiciel5
1.1. L'ordinateur vision bas niveau5
1.1.1. Traitement de 1 ' information5
1.1.2. Mémoires6
1.1.3. Microprocesseur8
1.1.4. Périphériques11
1.2. L'ordinateur vision haut niveau13
1.2.1. Modélisation du calcul13
1.2.2. Langages de haut niveau14
1.2.3. Du code source à l'exécutable15
Chapitre 2. Introduction à la sémantique des langages19
2.1. Environnement, mémoire, état19
2.1.1. Environnement d'évaluation19
2.1.2. Mémoire22
2.1.3. État24
2.2. Évaluation d'expressions24
2.2.1. Syntaxe25
2.2.2. Valeurs26
2.2.3. Sémantique d'évaluation28
2.3. Définition, affectation30
2.3.1. Définition d'un identificateur30
2.3.2. Affectation33
2.4. Exercices35
Chapitre 3. Sémantique des traits fonctionnels39
3.1. Aspects syntaxiques39
3.1.1. Syntaxe du noyau d'un langage fonctionnel39
3.1.2. Arbre syntaxique40
3.1.3. Raisonnement par induction sur les expressions43
3.1.4. Déclaration de variables, variables muettes, variables libres43
3.2. Sémantique d'exécution : fonction d'évaluation46
3.2.1. Erreurs lors de l'évaluation46
3.2.2. Valeurs47
3.2.3. Interprétation des opérateurs49
3.2.4. Fermeture50
3.2.5. Évaluation des expressions51
3.3. Sémantique d'exécution : sémantique opérationnelle58
3.3.1. Expressions simples59
3.3.2. Appel par valeur60
3.3.3. Fonctions récursives, fonctions mutuellement récursives64
3.3.4. Appel par nom65
3.3.5. Appel par valeur versus appel par nom67
3.4. Fonction d'évaluation versus relation d'évaluation68
3.4.1. Statut de la fonction d'évaluation68
3.4.2. Induction sur les arbres d'évaluation69
3.5. Propriétés sémantiques73
3.5.1. Expressions équivalentes74
3.5.2. Environnements équivalents75
3.6. Exercices76
Chapitre 4. Sémantique des traits impératifs81
4.1. Syntaxe du noyau d'un langage impératif81
4.2. Évaluation des expressions85
4.3. Évaluation des définitions90
4.4. Sémantiques opérationnelles93
4.4.1. Sémantique à grands pas93
4.4.2. Sémantique à petits pas97
4.4.3. Expressivité des sémantiques opérationnelles99
4.5. Propriétés sémantiques100
4.5.1. Programmes équivalents100
4.5.2. Terminaison de programmes102
4.5.3. Déterminisme de l'exécution des programmes104
4.5.4. Grands pas versus petits pas108
4.6. Procédures113
4.6.1. Blocs113
4.6.2. Fonctions en impératif : les procédures116
4.7. Autres approches122
4.7.1. Sémantique dénotationnelle122
4.7.2. Sémantique axiomatique, logique de Hoare133
4.8. Exercices138
Chapitre 5. Typage141
5.1. Quand et comment vérifier les types ?143
5.1.1. À quel moment vérifier les types ?143
5.1.2. Comment vérifier les types ?144
5.2. Typer informellement un programme Exp2145
5.2.1. Un premier exemple145
5.2.2. Typer une expression conditionnelle146
5.2.3. Typer sans contraintes de type146
5.2.4. Polymorphisme147
5.3. Règles de typage de Exp2148
5.3.1. Types, schémas de type, environnements de typage148
5.3.2. Généralisation, substitution, instanciation150
5.3.3. Règles et arbres de typage155
5.4. Algorithme d'inférence de type de Exp2158
5.4.1. Type principal159
5.4.2. Ensembles de contraintes et unification159
5.4.3. Algorithme d'inférence de type163
5.5. Propriétés172
5.5.1. Propriété du typage172
5.5.2. Propriétés de l'algorithme d'inférence172
5.6. Extension du typage aux constructions impératives173
5.6.1. Algèbre de types173
5.6.2. Règles de typage174
5.6.3. Typage des définitions polymorphes176
5.7. Sous-typage et surcharge177
5.7.1. Sous-typage178
5.7.2. Surcharge180
Chapitre 6. Types de données183
6.1. Types de base183
6.1.1. Booléens183
6.1.2. Entiers185
6.1.3. Caractères190
6.1.4. Flottants191
6.2. Tableaux195
6.3. Chaînes de caractères198
6.4. Définitions de types199
6.4.1. Abréviations de type199
6.4.2. Enregistrements200
6.4.3. Types énumérés205
6.4.4. Types somme206
6.5. Conditionnelle généralisée209
6.5.1. switch/case à la C210
6.5.2. Filtrage212
6.6. L'égalité221
6.6.1. Égalité physique221
6.6.2. Égalité structurelle223
6.6.3. Égalité entre fonctions225
Chapitre 7. Pointeurs et gestion de la mémoire229
7.1. Adresses et pointeurs229
7.2. Boutisme, endianness231
7.3. Pointeurs et tableaux231
7.4. Passage de paramètre par adresse232
7.5. Références235
7.5.1. Références en C++235
7.5.2. Références en Java240
7.6. Gestion de la mémoire240
7.6.1. Allocation de mémoire240
7.6.2. Libération de la mémoire244
7.6.3. Gestion automatique de la mémoire246
Chapitre 8. Exceptions251
8.1. Notifier et propager des erreurs251
8.1.1. Variable globale253
8.1.2. Définition d'enregistrement253
8.1.3. Passage par adresse254
8.1.4. Introduction des exceptions254
8.2. Une formalisation simple : les exceptions à la ML256
8.2.1. Syntaxe abstraite256
8.2.2. Valeurs256
8.2.3. Algèbre de types257
8.2.4. Sémantique opérationnelle257
8.2.5. Typage258
8.3. Exceptions dans d'autres langages259
8.3.1. Exceptions en OCaml259
8.3.2. Exceptions en Python260
8.3.3. Exceptions en Java261
8.3.4. Exceptions en C++262
Conclusion265
Annexe. Solution des exercices267
Liste des notations295
Liste des implantations des sémantiques297
Bibliographie301
Index303
Sommaire de Concepts et sémantique des langages de programmation 2307