Preuves de programmes et
méthodes formelles
Jean-Jacques Lévy
INRIA
Microsoft TechDays - 9 février 2010
Plan
• Logique de Hoare
– fibonacci
– terminaison
– drapeau hollandais
– formules et règles d'inférence
– fonctions récursives
• Logiques de programmes
• Mathématiques formelles
• Conclusion
Logique de Hoare
Trouver l'invariant !!!
Assertions
• les variables ont des valeurs modifiables
• une assertion est une propriété logique sur les valeurs de ces
variables !
• une assertion est attachée à un point du programme!
• on montre l'assertion de fin à partir de l'assertion d'entrée par
implications successives grâce à des assertions intermédiaires
Correction partielle – Correction totale
• dans un triplet , rien ne garantit que termine
• il y a correction partielle
• pour la correction totale, on utilise d'autres méthodes
(ordinaux, ...) pour démontrer la terminaison
• les assertions doivent correspondre aux spécifications
• il y a toujours un fossé entre spécifications et assertions
Logiques de programme
Hoare et le reste
tests environnements de programmation CAO matériel
analyse statique
vérification formelle spécification formelle
logique de Hoare
logiques temporelles
logique de la séparation
model checking logiques d’ordre supérieure
Hoare et le reste
tests environnements de programmation CAO matériel
emacs, visual studio, eclipse
analyse statique
astrée, slam, fluctuat
vérification formelle spécification formelle
logique de Hoare
logiques temporelles
krakatoa, spec#, frama-c
z, tla+
logique de la séparation
smallfoot
coq, isabelle, hol
model checking logiques d’ordre supérieure
bdds, sat solvers, smt (z3) pvs
Krak
atoa
Fram
a-C
Avec des pointeurs logiq
ue d
e la
sé p
arat
ion
static Liste miroir (Liste y, Liste x) {
while (x != null) {
Liste z = x.suivant;
x.suivant = y;
y = x; x = z;
}
return y;
}
miroir (null, x)
Invariant x�0 = x� · y où
x0 est la liste initiale
et
x� est l'image miroir de
x
Avec des pointeurs
• cet invariant n'est vrai que si les deux listes sont disjointes
• la logique de la séparation formule des propriétés par rapport à
un certain tas[o'hearn, reynolds]!
• un connecteur logique de base exprime que 2 tas sont disjoints!
• propriétés modulaires sur les tas mémoire!
• ...
Les diverses logiques de programme
• logique de Hoare pour programmes impératifs
• logique de la séparation pour programmes impératifs avec
pointeurs
• logique temporelle pour programmes concurrents
• logique d’ordre supérieur pour programmes fonctionnels et
mathématiques formelles
• démonstration automatique (model checking) pour calcul booléen
et logique sur domaines finis.
Mathématiques formelles
(logique mathématique)
Mathématiques formelles
• calcul booléen[bdds,sat solvers]
• logique de 1er ordre [smt solvers, z3, zenon]!
• logique de 1er ordre + théorie des ensembles [tla+]!
• logique d'ordre supérieure[coq, ssreflect]!
• ...
• théories utiles pour les preuves de programme
• théorème des 4 couleurs [gonthier], Feit-Thompson[?]
• ...
Conclusion
Quelques succès
• spécification système Météor (ligne 14) en Z [abrial]!
• analyse statique PV Ariane 5 [deutsch et al, inria]!
• analyse statique A380 [astrée, cousot et al, ens]!
• compilateur C minor certifié [leroy, inria]!
• slam/terminator/spec# teste les drivers de Windows [ball,
cook, leino, rajamani, msr]
• ...
• protocoles de sécurité[msr, inria, ens, cachan]
Futur
• méthodes formelles moins chères (bibliothèques, modularité)
• programmes certifiés (avec certificat vérifiable)
• langages de programmation avec plus de facilités pour des
spécifications logiques [F7]!
• environnements de programmation avec analyses statiques
• vérification des programmes mobiles!
• formation des ingénieurs
• processus biologiques vérifiés
