DEUG MIAS

INFORMATIQUE
Cours, TD, TP

Preuves de propriétés et de terminaison de programme

Sommaire

Introduction

Exemple de preuve de programme et Procédé général, pour les programmes non récursif

Exemple de preuve de programme récursifet Procédé général, pour les programmes récursif

1. Introduction

La vérification de propriétés de programmes utilise largement les raisonnements par induction. L'ambition n'est pas ici de faire une théorie des preuves de programmes mais simplement de montrer sur quelques exemples l'utilisation des raisonnements par induction dans ce domaine. Essentiellement, la récurrence est utile tant dans les boucles itératives que dans les procédés récursifs (procédures, fonctions, clauses . . . ).

Retour

2. Exemple de preuve de programme et Procédé général, pour les programmes non récursif

Considérons le programme suivant :

PROGRAMME carré

VAR a,b,c : entier

DÉBUT

LIRE a

SI a < 0 ALORS a := -a FINSI

b := a

c := O

TANT QUE b > 0 FAIRE

c := c + a

b := b - 1

FIN TANTQUE

AFFICHER c

FIN

Nous allons montrer que ce programme calcule et affiche a². La première chose à vérifier est que l'on finira par sortir de la boucle. On procède comme suit

Avant d'entrer dans la boucle, la valeur de b est un entier positif ou nul.
La valeur de b est décrémentée à chaque passage dans la boucle. Cette valeur finira donc par s'annuler.
Lorsque la valeur de b s'annule, on sort de la boucle.
On vient de prouver la terminaison de ce programme.

Un fois que l'on a prouvé que la boucle se termine, il faut s'assurer que le résultat est celui escompté. Pour ce faire, on montre que la propriété I(a, b, c):

"a² = c + b * a"

est vraie à chaque passage dans la boucle. Notons b_n et c_n les valeurs des variables b et c après le n-ième passage dans la boucle. Soit P(n) la propriété

"a² = c_n + b_n * a".

Il s'agit donc de vérifier que pour tout n dans N, P(n). On procède par récurrence.

On a b_o = a et c₀ = 0 donc P(0) est vraie.
Soit n dans N, supposons P(n). On a b_n+1 = b_n-1 et C_n+1 = C_n + a. On en déduit :

C_n+l+b_n+l *a=c_n+a+(b_n-1)*a=c_n+b_n*a=a²

ce qui prouve que P(n + 1) est vraie.

Lorsqu'on sort de la boucle on a donc à la fois b = O et I(a,b,c). Donc a² = c + O * a = c ce qui prouve que le résultat du programme est a².

De façon plus générale, considérons la boucle suivante où B désigne une expression booléenne et S une suite d'instructions

TANT QUE B FAIRE S FINTANTQUE

Pour montrer que la boucle termine, on lui associe une expression à valeurs dans un ensemble bien fondé. On montre ensuite que l'exécution de S fait décroître strictement la valeur de cette expression. Comme il n'y a pas de suite infinie strictement décroissante dans un ensemble bien fondé, on en déduit que la boucle se termine.
Pour montrer qu'une propriété P est vérifiée à la sortie de la boucle, on procède comme suit. On introduit une propriété annexe I appelée invariant de boucle. On montre ensuite que I est vérifiée avant l'entrée dans la boucle et qu'elle est conservée à chaque passage dans la boucle (c'est-à-dire si I est vraie avant l'exécution de S elle reste vraie après). Ceci constitue une preuve par récurrence du fait que la propriété I est vérifiée quel que soit le nombre de passages dans cette boucle. Finalement, on prouve que

¬B et I implique P

Puisque la propriété I est vraie après chaque passage dans la boucle, que l'on a prouvé que la boucle termine et qu'à ce moment B est fausse, ceci prouve bien que la propriété P est vraie à la sortie de la boucle.

EXERCICE : Montrer que le programme puissance se termine et affiche comme résultat an (avec la convention 0⁰ = 1).

PROGRAMME puissance 
	VAR a,n,r : entier 
DÉBUT 
	LIRE a,n 
	SI n < O et a = O 
		ALORS 
			AFFICHER résultat indéfini 
		SINON 
			r := 1 
			TANT QUE n < O FAIRE 
				r := r / a 
				n := n+1 
			FIN TANTQUE 

			TANT QUE n > O FAIRE 
				r := r * a 
				n := n-1 
			FIN TANTQUE 

			AFFICHER r 
	FIN SI
FIN

corrigé

Retour

3. Exemple de preuve de programme et Procédé général, pour les programmes récursif

Le cas des programmes récursifs est légèrement plus compliqué car il peut y avoir plusieurs appels récursifs dans un même programme et il peut y avoir aussi plusieurs cas où le résultat s'obtient sans appel récursif. Cependant, il se traite de façon analogue. Considérons la procédure suivante qui affiche l'écriture infixe d'un arbre binaire. On rappelle que la notation infixe (comme la notation polonaise inversée en est une autre, voir HP), la notation telle que l'opérateur est entre ses arguments.

PROCEDURE infixe (x : AB)

debut

SI x0 ALORS

infixe (filsGauche (x) )

AFFICHER racine (x)

infixe (filsDroit (x) )

FINSI

fin

Pour prouver sa terminaison, on considère par exemple la fonction h: AB N qui donne la hauteur d'un arbre binaire. La valeur de h(x) décroit strictement à chaque appel récursif, c'est-à-dire

h(filsGauche(x) < h(x)) et h(filsDroit(x)) < h(x).

Puisqu'il n'y a pas de suite infinie strictement décroissante dans N (voir ensembles bien fondés), on en déduit qu'il n'y a qu'un nombre fini d'appels récursifs. Par conséquent, la procédure infixe se termine toujours.

Il faut remarquer que le choix de la fonction h est arbitraire. On aurait aussi bien pu choisir la fonction n:AB N qui donne le nombre de noeuds d'un arbre ou même la fonction id: AB AB. En effet, la relation "être sous-arbre de" est une relation d'ordre bien fondée sur l'ensemble des arbres binaires AB. De plus, elle vérifie filsGauche(x) < x et filsDroit(x) < x ce qui prouve que la procédure infixe se termine.

De façon générale, pour prouver la terminaison d'un programme récursif on lui associe une expression à valeur dans un ensemble bien fondé. Le plus souvent, cette expression est uniquement fonction des arguments du programme récursif. Soit V la valeur de l'expression appliquée aux arguments du programme (V = h(x) dans l'exemple ci-dessus). Il faut alors vérifier que pour chaque appel récursif, la valeur de cette expression pour les paramètres de l'appel (h(filsGauche(x)) et h(filsDroit(x)) dans l'exemple ci-dessus) est strictement inférieure à V. On peut alors conclure que le programme termine.

De même, pour prouver une propriété d'un programme récursif, on lui associe une propriété P qui relie les arguments du programme à son résultat. On montre alors directement que P est vérifiée dans tous les cas où le programme se termine sans appel récursif. Puis en supposant la propriété vraie pour tous les appels récursifs du programme on prouve qu'elle est encore vraie à la fin du programme. Il s'agit donc encore d'une preuve par induction du fait que P est vraie à la fin du programme quels qu'en soient les arguments.

Considérons par exemple la fonction suivante:

FONCTION puissance(a,n)

DÉBUT

SI n = 0 ALORS

RETOURNE(1)

SINON

SI n = 1 ALORS

RETOURNE(a)

SINON

SI n est pair ALORS

RETOURNE(puissance(a * a, n / 2))

SINON

RETOURNE(a * puissance(a * a, (n - 1) / 2))

FINSI

FINSI

FINSI

FIN

Montrons que n > 0, cette fonction calcule aⁿ. On considère donc la propriété P: "puissance(a,n) = aⁿ" et on prouve qu'elle est vérifiée au retour de la fonction.

Il y a deux cas où la fonction retourne directement une valeur: si n = 0, le résultat est alors 1 = a⁰ et si n = 1, le résultat est alors a = a¹. La propriété P est donc vérifiée dans ces deux cas.

Si n est pair, le résultat est puissance(a * a, n/2). Or, par l'hypothèse d'induction on a puissance (a * a, n/2) = (a * a)n/2 = aⁿ. La propriété P est donc encore vérifiée.

 

De même, si n est impair, le résultat est a * puissance(a*a,(n- 1)/2). Par l'hypothèse d'induction on a

puissance(a * a, (n - 1)/2) = (a * a)(n-1)/2 = a^n-1.

On en déduit que le résultat est a * a^n-1 = aⁿ et la propriété P est encore vérifiée.

CQFD.

EXERCICE. Montrer que n N, I'appel Fact(n) de la fonction Fact définie ci-dessous, se termine et calcule n!

FONCTION Fact(n : entier) : entier

DÉBUT

SI n = 0 ALORS

RETOURNE(1)

SINON

RETOURNE(n*Fact(n-l))

FINSI

FIN

corrigé

Retour