Vérification des programmes impératifs :
la logique de HOARE
COMPAORE Anasthasie Joëlle
Qu’est-ce qu’un programme impératif ?
• Communément
– Suite d’instructions (affectations)
– Structures de contrôle
oExécution sous conditions (Conditionnelles)
oExécution itérative (boucles)
Idée maîtresse de la logique de HOARE
Programme = transformateur d’états
Etati exécution programme Etatj
État : valeurs des variables du programme
Exemple
{x = 2, y = 5} exécution programme P {x = 5, y = 2}
Caractéristiques méthodes de vérification
• Basées sur la preuve
• Semi-automatiques (utilisation d’heuristiques)
• Orientées propriétés
• Pendant ou après le développement
Pourquoi spécifier et vérifier les codes
• Spécification : composante documentation
• Peut diminuer de façon significative la durée du
développement et de la maintenance
• Facilite la réutilisation du code
• Peut être obligatoire pour les audits de certification
Un langage minimal
• E ::= n | x | (-E) | (E + E) | (E-E) | (E* E) |
(E div E) | (E mod E)
• B ::= true | false | (!B) | (B & B) | (B || B) |
(E == E) | (E != E) |
(E < E) | (E > E) | (E <= E) | (E >= E)
• C ::= x=E | C; C | if B {C1} else {C2} |
while B {C} | repeat {C} until B
Exemples de programmes
c = 0;
a = 0; a = x + 1;
while (a != 1) {
b = x; if ((a – 1) == 0) {
if (a mod 2 != 0) {
while (b >= y) { y = 1;
c=c+b;
b=b–y }
}
a = a + 1; else {
a = a div 2;
} y = a;
b = b * 2;
}
}; y = 1;
c = c + b; z = 0; début
y = 0;
while (z != x) {
while (y * y < x){
z=z+1
y = y + 1;
y = 1; y = y * z;
}
while (x != 0) { } y = y - 1;
y=y*x fin
x = x - 1;
}
Programme correct ?
Communément : Fait ce qu’il est censé faire sans
se tromper, dans les conditions déterminées
Nécessité de décrire (formellement)
• Le quoi : que doit faire le programme ?
• Les cas pris en compte : sous quelles conditions ?
Exemple : spécifier la division entière de x par y ?
• Le quoi : trouver a et b tel que x = (y * a) + b et
y>b
• Les cas : x entier, y entier non nul
Expression de la spécification
Relation entre :
• les entrées :
o valeurs des variables avant exécution,
o arguments des fonctions
o etc.
• les sorties :
o valeurs des variables après exécution
o etc.
Rappel des notations logiques usuelles
• True
• False
• ¬P
• p Ʌ q signifie p «et» q
• p V q signifie p «ou» q
• p q signifie p «implique» q
• x, p signifie «quelque soit x, p est vrai »
• Ǝ x, p signifie «il existe x tel que p est vrai »
Spécification : triplets de HOARE
{P} prog {Q} : = triplet de HOARE
• P = Pré-condition
Formules de logique
• Q = Post-condition
• Prog = programme spécifié
Si « prog » s’exécute dans un état satisfaisant P,
l’état issu de l’exécution de « prog » satisfera Q
Spécification : triplets de HOARE
Deux types de variables
• Variables de programme : apparaissent dans le programme
• Variables logiques :
– n’apparaissent pas dans le programme
– Servent en général à conserver les anciennes valeurs des variables de
programme
Exemple : spécifier le programme qui inverse deux valeurs
{x = x0 y = y0} Inverse {x = y0 y = x0}
Spécification : triplets de HOARE
Remarques/définitions
• Un état est une fonction qui associe des valeurs à
chaque variable (pertinente)
• Les quantificateurs ne lient que les variables
n’apparaissant pas dans « prog »
• Lorsqu’il n’est pas nécessaire de contraindre l’état initial,
on utilise T comme précondition
Exercice : Spécifier les programmes présentés
Notion (formelle) de correction
Programme correct = triplet de HOARE vrai
Définition (correction partielle) : Un triplet de HOARE
{P}prog{Q} est satisfait pour la correction partielle
(|=par (P) prog (Q)) si :
pour tout état satisfaisant P,
si prog termine alors
l’état résultant de l’exécution de prog satisfait Q
|=par : relation de satisfaction pour la correction partielle
Notion (formelle) de correction
Définition (correction totale) : Un triplet de HOARE
{P}prog{Q} est satisfait pour la correction totale
(|=tot (P) prog (Q)) si :
pour tout état satisfaisant P,
prog termine et
l’état résultant de l’exécution de prog satisfait Q
|=tot : relation de satisfaction pour la correction totale
Notion (formelle) de correction
Définition : si la correction partielle (totale) d’un triplet
peut être prouvée dans le calcul de correction partielle
(totale), le séquent
|--par (P) prog (Q) (|--tot (P) prog (Q)) est valide
Règles de calcul de la correction partielle
règle de HOARE : règle de déduction dans laquelle
les jugements sont des triplets de HOARE
triplet1 tripletn
triplet
Triplet t correct : il existe un arbre de déduction de
HOARE complet ayant comme racine t.
Règle de l’affectation
Notations
• x=E
• P[x E] ou P[E/x]: P où x est remplacée par E
AFF1
{P[x E]} x=E {P}
AFF2
{P} x = E {P[x x0] Ʌ x == E [xx0]}
Règle de l’affectation
Exemples :
1) On suppose prog : x = 2. Lesquels de ces triplets
sont vrais ?
a) {2 = 2} Prog {x = 2} c) {2 = y} Prog {x = y}
b) {2 = 4} Prog {x = 4} d) {2 > 0} Prog {x > 0}
2) On suppose prog : x = x + 1. Trouver P pour que
les triplets suivants soient vrais
a) {?} Prog {x = 2} c) {?} Prog {x+5 = y}
b) {?} Prog {x = y} d) {?} Prog {x > 0 y > 0}
3) Compléter : {x-y >= 0} y = y+x {?}
Règles de la séquence et de la conséquence
C1; C2
{P} C1 {Q} {Q} C2 {R}
SEQ
{P} C1; C2{R}
P P’ {P’} C {Q’} Q’ Q
CONSEQ
{P} C{Q}
Règles de la séquence et de la conséquence
Exemples :
1) Montrer que u = x + y après l’exécution de :
z = x;
z = z + y;
u = z;
2) Montrer que
• {y = 5} x = y + 1 {x = 6}
• {y < 3} y = y + 1 {y < 4}
• {x=0} x = x+1;x=x+1 {x = 2}
sont valides
Règle de la conditionnelle
Notation : if B then C1 else C2
{P Ʌ B} C1 {Q} {P Ʌ ¬B} C2 {Q}
COND
{P} if B then C1 else C2 {Q}
Exemple :
{true} if y = 0 then x = y else x = 0 {x=0}
{true} a = x + 1; if (a – 1 == 0) y = 1 else y = a {y = x+1}
Règle de l’itération
Notation : while B {C}
{P Ʌ B} C {P}
Partial-WHILE
{P} while B {C} {P Ʌ ¬B}
Invariant déjà donné (P)
Exemple :
•{x>=0} while (x<b) {x := x+1} {x>=0 Ʌ ¬(x <b)}
Règle de l’itération
{ Ʌ B} C {}
Partial-WHILE
{} while B {C} {}
Preuve en remontant
1. Trouver un invariant :
2. Essayer de prouver que |-- B et |-- . Si échec retour à 1, sinon
poursuivre
3. Partir de comme post-condition de la boucle et remonter jusqu’à la
première instruction de la boucle. On note ’ la caractérisation de l’état à ce
niveau
4. Essayer de prouver que |-- B ‘ est valide. Si OK ( est un invariant),
poursuivre, sinon retour en 1)
5. Écrire au dessus du while (et au dessus de ce s’il n’y a pas des
instructions avant le while) en annotant ce avec l’implication
Règle de l’itération
Exemple : correction partielle du programme ci-dessous
y = 1;
z = 0;
while (z != x) {
z=z+1
y = y * z;
}
Calcul de la correction totale
Deux étapes
1. Correction partielle
2. Terminaison de prog
Généralement dans cet ordre
Calcul de la correction totale
Terminaison
1. Recherche d’un variant de boucle
{P’ Ʌ B Ʌ 0 <= E = E0} C {P’ Ʌ 0 <= E < E0}
Total-WHILE
{P’ Ʌ 0 <= E} while B {C} {P’ Ʌ ¬B}
Exemple :
{x>=0} while x<b do x := x+1 done {x>=0 Ʌ ¬(x <b)}
