[PDF] Structures de données et méthodes formelles

View - Download Structures de données et méthodes formelles

Previous PDF

Next PDF

Structures de données

et méthodes formelles

Springer

Paris

Berlin

Heidelberg

New York

Hong Kong

Londres

Milan Tokyo

Marc Guyomard

Structures de données

et méthodes formelles

Marc Guyomard

Enssat Irisa

Université de Rennes 1

Technopole Anticipa

6, rue de Kerampont

BP 80518

22305 Lannion Cedex

ISBN : 978-2-8178-0199-5 Springer Paris Berlin Heidelberg New York

© Springer-Verlag France, 2011

Imprimé en France

Springer-Verlag est membre du groupe Springer Science + Business Media

Cet ouvrage est soumis au copyright. Tous droits réservés, notamment la reproduction et la repré-

sentation, la traduction, la réimpression, l"exposé, la reproduction des illustrations et des tableaux,

la transmission par voie d"enregistrement sonore ou visuel, la reproduction par microfi lm ou tout

autre moyen ainsi que la conservation des banques de données. La loi française sur le copyright du

9 septembre 1965 dans la version en vigueur n"autorise une reproduction intégrale ou partielle que

dans certains cas, et en principe moyennant le paiement des droits. Toute représentation, reproduc-

tion, contrefaçon ou conservation dans une banque de données par quelque procédé que ce soit est

sanctionnée par la loi pénale sur le copyright.

L"utilisation dans cet ouvrage de désignations, dénominations commerciales, marques de fabrique, etc.

même sans spécifi cation ne signifi e pas que ces termes soient libres de la législation sur les marques de

fabrique et la protection des marques et qu"ils puissent être utilisés par chacun.

La maison d"édition décline toute responsabilité quant à l"exactitude des indications de dosage et

des modes d"emploi. Dans chaque cas il incombe à l"usager de vérifi er les informations données par

comparaison à la littérature existante. Maquette de couverture : Jean-François Montmarché

Illustrations de couverture : (Fotolia.com)

programming layout © Mike Kiev #11376759 circuit imprimé © Sylvie Thenard #8582813

Connected shape algorithm © 1xpert #29471089

COLLECTION Télécom

Directeur de la Collection : Pierre-Noël Favennec

COMITÉ SCIENTIFIQUE

Président

: Claude Guéguen

Michel Allovon (Orange Labs)

Chantal Ammi (Télécom Ecole de management)

Annie Blandin (Télécom Bretagne)

Jean-Pierre Cocquerez (UTC Compiègne, GDR ISIS)

Frédérique de Fornel (ICB Dijon, GDR Ondes)

Georges Fiche (APAST Lannion)

Alain Hillion (Télécom Bretagne)

René Joly (Télécom ParisTech)

Henri Maître (Télécom ParisTech)

Chantal Morley (Télécom SudParis)

Gérard Pogorel (Télécom ParisTech)

Gérard Poulain (APAST Lannion)

Serge Proulx (UQAM Montreal)

Nicolas Puech (Télécom ParisTech)

Guy Pujolle (UPMC Paris)

Pierre Rolin (Télécom SudParis)

Basel Solaiman (Télécom Bretagne)

Sami Tabbane (SupCom Tunis)

Joe Wiart (Orange Labs)

À Éveline,

David, Astrid et Christophe

Orlane, Sirina, Émilie, Vic

... I have no objection with people feeling more comfortable with the word EnglishŽ replacing the word mathematicsŽ.

I just wonder whether such people

are not assigning themselves a more difficult task... ... Je n"ai rien à objecter aux personnes qui se sentent plus à l"aise quand le mot " français » remplace le mot " mathématiques ».

Je me demande simplement

dans quelle mesure ces personnes ne se compliquent pas la tâche...

J.-R. Abrial

, The B-Book, 1996.

Préface

Le cours de mathématiques pour l"informatique, de même que le cours de logique des propositions et des prédicats du premier ordre font encore partie de la formation de base des informaticiens. Ainsi les départements d"informatique, dès la création desiut, ont-ils bénéficié d"enseignements de mathématiques pour l"informatique et d"enseignements de logique alors même que la formation dure deux ans et que la plupart des étudiants, il y a 40 ans, ne poursuivaient pas leurs études. Mais, trop souvent, l"utilisation des mathématiques demeure fort limitée pour ne pas dire absente dans le processus qui mène de la spécification du problème à la construction du logiciel. Marc Guyomard présente, dans cet ouvrage, une approche de la construction des algorithmes relatifs aux structures de données, une approche par la preuve. C"est le livre d"un sage!Sapiens ni- hil armat quod non probet.L"auteur délivre à la fois un cours original sur les structures de données et une méthode formelle de construction de programmes. Ce livre est au cœur de l"informatique. Il suffit d"y lire les applications des diffé- rentes structures de données, pour constater que l"informatique du XXI e siècle fait un grand usage des structures manipulées dans ce livre.Structures de don- nées et méthodes formellestraite des fondements sans lesquels, malgré la puis- sance actuelle des machines, nous ne disposerions pas des logiciels performants qui sont à la disposition de tous aujourd"hui. Et ceux qui ont utilisé différents systèmes d"exploitation bien connus fournis avec les micro-ordinateurs, peuvent les donner en exemples de la " loi de Reiser » - appelée sur la Toile " Loi de Wirth » alors que N. Wirth ne fait que citer M. Reiser : " Le logiciel ralentit

plus vite que le matériel n"accélère. » L"Église catholique en était-elle peut-être

consciente en choisissant comme saint patron des informaticiens Isidore de Sé- ville qui, d"après ce que l"on peut lire, répété de nombreuses fois sur la Toile - ce qui n"est pas un gage de vérité 1 même si c"est un critère pour améliorer son " page rank » -, aurait inventé les " tries » (l"une des structures étudiées dans ce livre), qui sont appliqués dans son ouvrage célèbre, les Etymologies. Leibniz disait :Sedemus et calculemus,asseyons-nous et calculons. C"est ce que propose Marc Guyomard. Son point de départ est une spécification écrite en utilisant la mathématique élémentaire sur les ensembles et les relations ainsi que la logique des prédicats (le quoi), spécification à partir de laquelle il dérive - il calcule - la représentation des algorithmes (le comment). Il utilise la notation de la méthode B mise au point par Jean-Raymond Abrial, méthode qui a maintenant fait la preuve de son intérêt pédagogique et opérationnel. La notation est en grande

1. En fait, comme le note Donald Knuth dans le tome 3 de son monumentalThe Art of

Computer Programmingcité parmi les douze meilleures monographies du siècle par lAmerican

Scientist... les "Étymologies» sont ordonnées selon un ordre lexicographique imparfait, portant

uniquement sur la première lettre. De là aux tries, il y a un long chemin !... x Structures de données et méthodes formelles partie celle qu"utilisent couramment les mathématiciens et les logiciens, com- plétée par des symboles fort pratiques. Nous pensons à ce propos qu"il est sans doute plus profitable d"enseigner une partie des programmes de mathématiques dans le cadre de l"enseignement de spécification/programmation que d"en faire des enseignements cloisonnés. L"avantage qui en résulte est de rapprocher l"outil (les mathématiques) de sa principale application (la spécification), compétence au cœur du métier d"informaticien. Ainsi on peut mettre l"accent sur une activité essentielle, celle d"abstraction. La méthode B opère par raffinage, afin de passer de l"abstrait (la spécification) au concret (l"algorithme rédigé dans un langage exécutable sur un ordinateur) et à satisfaire en cours de processus, des obliga- tions de preuves, preuves qui peuvent être assistées par des logiciels. Comme il a réutilisé les spécifications ensemblistes et la logique, Marc Guyomard réutilise le modèle fonctionnel en programmation, modèle très souvent enseigné à juste raison, et il l"applique lors de la dérivation de programmes au lieu d"appliquer le cadre algorithmique. Voilà sur quoi repose l"originalité de la démarche pré- sentée et appliquée par Marc Guyomard dans ce livre. Il a renouvelé le fameux " structure de données + algorithmes = programmes » de N. Wirth en énon- çant " spécifications + fonction d"abstraction + calcul = programme ». Il lui restait à choisir quelles structures de données présenter et dans quel ordre. Il a choisi une perspective historique, perspective trop peu souvent utilisée dans les enseignements d"informatique où l"on a parfois tendance à considérer qu"une bibliographie de plus de 5 ans d"âge n"a pas sa place dans une publication. Nous avions été séduit par les remarquables polycopiés de Marc Guyomard, en parti- culier un cours sur la compilation et un autre sur la construction de la boucle. C"est avec plaisir que nous avons appris que Marc Guyomard allait diffuser son cours sur les structures de données qu"il dispense aux étudiants de l"Enssat de Lannion. Je suis sûr que les enseignants, les étudiants, les praticiens apprécieront ce livre qui leur fournit à la fois, une présentation raisonnée de très nombreuses structures de données, bien plus que ce que l"on trouve habituellement dans les livres comparables, et une méthode originale de développement de programmes fondé sur la preuve. Toutes les notions et les notations nécessaires pour suivre l"exposé sont présentées, lorsque le besoin s"en fait sentir,Structures de données et méthodes formellesest un livre que les programmeurs doivent avoir à portée de la main.

Henri Habrias

Professeur émérite à l"Université de Nantes

Table des matières

Préfaceix

Avant-propos1

ILesbases13

1 Mathématiques pour la spécification et les structures

de données15

1.1 Introduction.............................. 15

1.2 Raisonnement............................. 18

1.3 Calculpropositionnel......................... 21

1.4 Calculdesprédicats ......................... 22

1.4.1 Quanti“cationuniverselle .................. 22

1.4.2 Deuxnouveauxtypesd"expressions............. 25

1.5 Égalité................................. 26

1.6 Théoriedesensembles ........................ 27

1.6.1 Opérationsensemblistestraditionnelles........... 29

1.6.2 Choixdansunensemble................... 30

1.6.3 Relationsbinaires ...................... 31

1.6.4 Fonctions ........................... 34

1.7 Ensembles particuliers........................ 36

1.8 Exempledemodélisationensembliste................ 40

1.9 Construction de structures inductives................ 43

1.10Démonstrationparrécurrence.................... 43

1.11Opérations .............................. 47

1.11.1Introduction ......................... 47

1.11.2Expressionpréconditionnée ................. 48

1.11.3Dé“nitiondesopérations .................. 48

1.11.4Évaluationdesopérations.................. 50

1.11.5 Propagation des préconditions............... 52

1.12Conclusionetremarquesbibliographiques ............. 56

xii Structures de données et méthodes formelles

2 Spécifications+Fonction d"abstraction+Calcul=Programme 59

2.1 Cadregénéraldeladémarche.................... 59

2.2 Formalismepourlestypes-Exemple................ 61

2.3 Calculdesopérations-Exemple .................. 64

2.3.1 Calcul d"une représentation de l"opérationplus_n.... 66

2.3.2 Calcul d"une représentation de l"opérationinf_n..... 68

2.4 Induction, support et renforcement................. 71

2.5 Conclusion .............................. 75

3 Étude de quelques structures outils77

3.1 Listesfinies.............................. 78

3.1.1 Présentationinformelle ................... 78

3.1.2 Ébauchedeconstruction................... 79

3.1.3 Opérationssurleslistes................... 82

3.1.4 Notationlinéaire....................... 82

3.2 Arbresfinis .............................. 83

3.3 Arbresnonordonnés......................... 85

3.3.1 Introduction : les arbres non ordonnés non étiquetés . . . 85

3.3.2 Arbresnonordonnésétiquetés ............... 85

3.4 Arbresplanaires ........................... 87

3.4.1 Introduction:lesarbresplanairesnonétiquetés...... 87

3.4.2 Arbresplanairesétiquetés.................. 87

3.5 Arbresn-aires............................. 88

3.5.1 Introduction:lesarbresn-airesnonétiquetés....... 88

3.5.2 Lesarbresbinairesétiquetés................. 89

3.6 Arbres binaires partiellement étiquetés : les arbres externes . . . 96

3.6.1 Présentationinformelle ................... 96

3.6.2 Ébauchedeconstruction................... 97

3.6.3 Opérationssurlesarbresexternes ............. 98

3.6.4 Conclusion .......................... 98

3.7 Sacsfinis ............................... 100

3.7.1 Présentationinformelle ................... 100

3.7.2 Ébauchedeconstruction................... 101

3.7.3 Opérationssurlessacs.................... 102

3.7.4 Propriétésdessacs...................... 103

3.8 Conclusionetremarquesbibliographiques ............. 104

4 Analyse d"algorithmes107

4.1 Notationsasymptotiques....................... 108

4.2 Analyse classique de la complexité

defonctions.............................. 113

4.2.1 Passage du texte d"une fonction à une équation

récurrente........................... 114

4.2.2 Complexité la meilleure, la pire, moyenne......... 116

4.2.3 Résolutiond"équationsrécurrentes ............. 117

4.2.4 Contourner ou simplifier certaines étapes

intermédiaires......................... 120

Table des matières xiii

4.2.5 Conclusionetremarquesbibliographiques......... 122

4.3 Analyse amortie de la complexité -

laméthodedupotentiel ....................... 123

4.3.1 Introduction ......................... 123

4.3.2 Fondementsthéoriquesdelaméthodedupotentiel.... 125

4.3.3 Exemple............................ 126

4.3.4 Conclusionetremarquesbibliographiques......... 128

5 Exemples129

5.1 Premierexemple ........................... 129

5.1.1 Spécificationdutypeabstrait ............... 129

5.1.2 Définition du support concret................ 130

5.1.3 Définitiondelafonctiond"abstraction........... 130

5.1.4 Spécificationformelledesopérations............ 131

5.1.5 Calculdelareprésentationdesopérations......... 131

5.1.6 Complexités de l"opérationsuc_l.............. 135

5.1.7 Conclusionetremarquesbibliographiques......... 138

5.2 Secondexemple............................ 139

5.2.1 Spécification du type abstraitensnat........... 139

5.2.2 Définition du support concret................ 139

5.2.3 Définitiondelafonctiond"abstraction........... 140

5.2.4 Spécificationdesopérationsconcrètes ........... 140

5.2.5 Calcul d"une représentation de l"opérationeAjout_l... 140

5.2.6 Conclusion .......................... 143

II Structures de données fondamentales :spéci“cation et mises en œuvre 145

6 Ensembles de clés scalaires147

6.1 Présentationinformelle........................ 147

6.2 Spécification du type abstraitensabst............... 148

6.3 Méthodesarborescentes:lesarbresbinairesderecherche..... 150

6.3.1 Définition du support concret................ 150

6.3.2 Définitiondelafonctiond"abstraction........... 151

6.3.3 Spécificationdesopérationsconcrètes ........... 151

6.3.4 Calcul de la représentation des opérations concrètes . . . 151

6.3.5 Conclusionetremarquesbibliographiques......... 168

6.4 Méthodesdehachage......................... 169

6.4.1 Introduction ......................... 169

6.4.2 Définition du support concret................ 171

6.4.3 Définitiondelafonctiond"abstraction........... 172

6.4.4 Spécificationdesopérationsconcrètes ........... 172

6.4.5 Calcul de la représentation des opérations concrètes . . . 172

6.4.6 Fonctiondehachage..................... 175

6.4.7 Autresméthodesdehachage ................ 175

6.4.8 Conclusionetremarquesbibliographiques......... 177

6.5 Méthodesarborescentes:lesarbresexternesderecherche .... 178

xiv Structures de données et méthodes formelles

6.5.1 Définition du support concret................ 178

6.5.2 Définitiondelafonctiond"abstraction........... 179

6.5.3 Spécificationdesopérations................. 179

6.5.4 Calcul de la représentation des opérations concrètes . . . 179

6.5.5 Renforcement du support par décomposition de la fonction

max.............................. 187

6.5.6 Conclusionetremarquesbibliographiques......... 190

6.6 Méthodes équilibrées : lesAvl................... 191

6.6.1 Introduction ......................... 191

6.6.2 Définitionetpropriétésdusupportconcret ........ 192

6.6.3 Définitiondelafonctiond"abstraction........... 196

6.6.4 Spécificationdesopérationsconcrètes ........... 196

6.6.5 Rotations........................... 197

6.6.6 Calcul de la représentation des opérations concrètes . . . 202

6.6.7 Renforcement du support par décomposition du rayon . . 213

6.6.8 Conclusionetremarquesbibliographiques......... 214

6.7 Méthodes équilibrées : les B-arbres................. 216

6.7.1 Introduction ......................... 216

6.7.2 Définition du support concret................ 218

6.7.3 Définitiondelafonctiond"abstraction........... 227

6.7.4 Spécificationdesopérationsconcrètes ........... 228

6.7.5 Calcul de la représentation des opérations concrètes . . . 228

6.7.6 Conclusionetremarquesbibliographiques......... 243

6.8 Structures autoadaptatives et analyse amortie :

lesarbresdéployés .......................... 245

6.8.1 Introduction ......................... 245

6.8.2 Principedel"insertiondansunarbredéployé ....... 245

6.8.3 Support concret et fonction d"abstraction......... 246

6.8.4 Calcul de l"opérationeAjout_ad.............. 247

6.8.5 Analyse amortie de l"opérationeAjout_ad........ 251

6.8.6 Conclusionetremarquesbibliographiques......... 257

6.9 Méthodesaléatoires:lestreapsrandomisés ............ 258

6.9.1 Définition du support concret................ 258

6.9.2 Définitiondelafonctiond"abstraction........... 259

6.9.3 Spécificationdesopérationsconcrètes ........... 260

6.9.4 Calcul de la représentation des opérations concrètes . . . 260

6.9.5 Renforcer ou non le support ?................ 268

6.9.6 Treapsrandomisés ...................... 268

6.9.7 Conclusionetremarquesbibliographiques......... 270

7 Ensembles de clés structurées273

7.1 Ensembles de chaînes, représentation par tries........... 273

7.1.1 Introduction ......................... 273

7.1.2 Définitiondessupportsconcrets .............. 274

7.1.3 Définitiondesfonctionsd"abstraction ........... 276

7.1.4 Spécificationdesopérationsconcrètes ........... 277

7.1.5 Calcul de la représentation des opérations concrètes . . . 277

Table des matières xv

7.1.6 Variantesdestries ...................... 286

7.1.7 Conclusionetremarquesbibliographiques......... 291

7.2 Ensembles de couples, représentation parkd-arbres........ 293

7.2.1 Ensembles de couples, spécification abstraite....... 293

7.2.2 Ensembles de couples, introduction auxkd-arbres..... 295

7.2.3 Définition du support concret................ 296

7.2.4 Définitiondelafonctiond"abstraction........... 298

7.2.5 Spécificationdesopérationsconcrètes ........... 298

7.2.6 Calcul d"une représentation des opérations concrètes . . . 299

7.2.7 Conclusionetremarquesbibliographiques......... 309

8 Files simples313

8.1 Présentationinformelledesfilessimples .............. 313

8.2 Spécification du type abstraitfileabst.............. 314

8.3 Miseenœuvre"chaînée»...................... 315

8.3.1 Définition du support concret................ 318

8.3.2 Définitiondelafonctiond"abstraction........... 318

8.3.3 Spécificationformelledesopérations............ 318

8.3.4 Calcul de la représentation des opérations concrètes . . . 318

8.3.5 Complexitédelamiseenœuvrechaînée.......... 322

8.3.6 Conclusionetremarquesbibliographiques......... 324

9 Files de priorité327

9.1 Présentationinformelle........................ 327

9.2 Spécification du type abstraitfpabst............... 328

9.3 Méthodes équilibrées : les tas.................... 329

9.3.1 Principe............................ 329

9.3.2 Conclusionetremarquesbibliographiques......... 331

9.4 Méthodes équilibrées : les files binomiales............. 331

9.4.1 Définition des supports concrets.............. 333

9.4.2 Définitiondesfonctionsd"abstraction ........... 335

9.4.3 Spécificationdesopérationsconcrètes ........... 336

9.4.4 Calcul de la représentation des opérations concrètes . . . 339

9.4.5 Renforcement du support par décomposition du rayon . . 358

9.4.6 Conclusionetremarquesbibliographiques......... 360

9.5 Méthodes autoadaptatives : les minimiers obliques (skew heaps) . 361

9.5.1 Définition du support concret................ 362

9.5.2 Définitiondelafonctiond"abstraction........... 363

9.5.3 Spécificationdesopérationsconcrètes ........... 363

9.5.4 Calcul d"une représentation des opérations concrètes . . . 363

9.5.5 Analyse amortie de l"opérationfus............. 368

9.5.6 Conclusionetremarquesbibliographiques......... 373

10 Tableaux "exibles377

10.1Introduction.............................. 377

10.2 Flexibilité faible à droite : présentation informelle......... 378

10.3 Flexibilité faible : spécification du type abstrait.......... 378

10.4 Flexibilité faible : mise en œuvre par arbres de Braun...... 378

xvi Structures de données et méthodes formelles

10.4.1 Flexibilité faible : définition du support concret...... 381

10.4.2 Flexibilité faible : définition de la fonction d"abstraction . 382

10.4.3 Flexibilité faible : spécification des opérations concrètes . 384

10.4.4 Flexibilité faible : calcul des opérations concrètes..... 385

10.4.5 Décomposer la fonctionw?................. 391

10.4.6Conclusionetremarquesbibliographiques......... 391

10.5 Flexibilité forte : présentation informelle.............. 394

10.6 Flexibilité forte : spécification du type abstraittsabst...... 395

10.7 Flexibilité forte : mise en œuvre par minimiers.......... 395

10.7.1Principe............................ 395

10.7.2Conclusionetremarquesbibliographiques......... 398

Annexes ... Répertoire de propriétés401

A Propriétés générales des ensembles403

B Propriétés des relations binaires405

C Propriétés des fonctions411

D Propriétés des entiers413

E Opérateurs et priorités415

Bibliographie417

Index425

Avant-propos

Un de plus !Un ouvrage de plus sur les structures de données ! Mais pour- quoi diable ? Tout a été dit et écrit dans ce domaine. En témoignent les centaines

de livres publiés depuis lavènement de linformatique. Cest peut-être la ré"exion

que se fait le lecteur en ce moment. Pourtant il lui suffit de feuilleter louvrage quil tient entre ses mains pour constater que le présent livre se démarque de la plupart de ses homologues : il est émaillé de nombreuses formules, de démons- trations, de programmes qui ne sont rédigés ni en C ni en Java ni en Perl. Cest que linformatique logicielle est engagée depuis quelques décennies déjà dans un processus irréversible de rationalisation. Elle a dores et déjà acquis le statut de

science. Cest particulièrement visible à travers les avancées régulières de ce quil

est convenu dappeler les " méthodes formelles pour le génie logiciel ». Cette approche de linformatique a déjà fait de nombreux adeptes dans lindustrie, notamment pour la réalisation de systèmes critiques (transports, énergie, méde- cine, télécommunications, etc.). En ce qui concerne lenseignement, en général les formations du supérieur incluent dans leur ore pédagogique un module sur cequotesdbs_dbs46.pdfusesText_46

[PDF] Les subordonnées : Alors que et tandis que, ils expriment l'opposition, le temps ou les deux

[PDF] LES SUBORDONNES SVP !!

[PDF] Les substances edeine et cyclhoheximide agissent a deux phases differents d'une des etapes de la synthese de protine

[PDF] Les substitus et leurs référents!Urgent besoin d'aide!!!

[PDF] les substituts exercices

[PDF] les substituts grammaticaux 1am

[PDF] les substituts grammaticaux et lexicaux exercices français facile

[PDF] les substituts grammaticaux exercices 3am

[PDF] les substituts grammaticaux pdf

[PDF] les substituts lexicaux et grammaticaux 3am

[PDF] les substituts lexicaux et grammaticaux exercices corrigés pdf

[PDF] Les succès de L'Union Européenne

[PDF] Les Sud : Croissance Démographique et Richesses

[PDF] les suffixes et les préfixes

[PDF] les suite