Spécification et Certification du Logiciel
Ce cours est une introduction à l'utilisation des
méthodes formelles dans le développement du
logiciel.
Les méthodes de spécification et validation du logiciels
dites formelles reposent sur l'utilisation dans le domaine de
l'informatique des travaux développés depuis le
début de ce siècle dans le domaine de la logique
mathématique. Elles en héritent rigueur et
précision qui sont autant d'avantages pour le contrôle de la
qualité et de la correction du logiciel.
Le cours s'articule en trois parties :
- 1.
- un rappel indispensable des bases de la logique formelle
ainsi que de la théorie des ensembles.
- 2.
- une présentation de la méthode des assertions
initiée par Hoare et Dijkstra qui permet une certification a
posteriori des programmes impératifs.
- 3.
- une présentation de la méthode B due à Abrial qui
met en oeuvre la technique du développement de programmes par
raffinement.
Notes de cours
- Introduction : un plaidoyer pro domo pour l'usage des
méthodes formelles
(c1.ps)
- Calcul des propositions : syntaxe, sémantique,
déduction naturelle, calcul des séquents, correction et
complétude du calcul des séquents, élmination des
coupures pour le calcul des séquents, décidabilité
(c2.ps)
- Calcul des prédicats : syntaxe, sémantique, etc ...
(c3.ps)
- Théries axiomatiques : l'égalité,
l'arithmétique formelle, types de donnée, les listes
(c4.ps)
- Equations, fonctions et spécification : exemples
(c5.ps)
- Théorie des ensembles : Zermelo, relations, fonctions
(c6.ps)
Page initiale Maison
Page précédente Enseignement