Academie pro

Liste des matières

Mathématiques :

Preuves de programmes

Objectifs Spécifiques :

1 Introduction à la preuve de programmme 1
I Informations pratiques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
II Qu'est-ce que la preuve de programme ? . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
II.1 Problématique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
II.2 Quelles propriétés prouver ? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
II.3 Quelles méthodes d'analyse des programmes ? . . . . . . . . . . . . . . . . . . . . . 2
III Preuves sur papier . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
III.1 Programmes impératifs (Invariants et terminaison) . . . . . . . . . . . . . . . . . . 2
III.2 Programmes récursifs (Principe d'induction) . . . . . . . . . . . . . . . . . . . . . . 3
2 Logique de Hoare 5
I Installer et se documenter . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
II Principes de la logique de Hoare . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
III Preuves en logique de Hoare . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
III.1 Règles de la logique de Hoare . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
III.2 Correction de la logique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
III.3 Annoter les programmes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
III.4 Preuves de terminaison . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
IV Calcul de plus faible pré condition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
V Automatisation des preuves . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
3 L'assistant à la preuve Coq 15
I Installer et se documenter . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
II Correspondance de Curry-Howard . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
II.1 Lambda-calcul simplement typé . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
II.2 Logique minimale intuitionniste . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
II.3 Correspondance de Curry-Howard . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
II.4 L'assistant à la preuve Coq . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
III Les inductifs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
III.1 Types inductifs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
III.2 Prédicats inductifs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
IV Spécication et certication des programmes en Coq . . . . . . . . . . . . . . . . . . . . . 23
IV.1 Preuve de programme, un exemple . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
IV.2 Spécier les fonctions partielles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
IV.3 Spécier avec les types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25

Ressources disponibles :


Cours 1 Travaux dirigés 1 Travaux pratiques 0 Contrôle continu 0 Examen terminal 0

Mme. Tassonpp Christine | Université Paris Diderot

Cours

Cours de preuves de programmes


télécharger Cours de preuves de programmes

Td

TD et TP de preuves de programmes


télécharger TD et TP de preuves de programmes



Livres populaires