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

CORRECTION

Preuve de terminaison

Les problèmes pour cette preuve sont localisés dans les deux boucles tant que.

Pour entrer dans la 1er boucle il faut n<0 (et a0). La valeur de n est incrémentée à chaque passage dans cette boucle. La condition de continuité est n<0, comme n finira par s'annuler, on sortira en temps fini de cette boucle. Quand on sort de la la 1er boucle on a n=0.

Pour d'entrer dans la seconde boucle il faut n>0. De la même manière que précédement, on va sortir de cette boucle avec n=0.

(iii)En conclusion soit on passe dans une de ces boucles (on avait alors n0 à l'origine), en sortie (niveau afficher r) on a n=0, soit on passe dans aucune des 2 boucles et n=0 à l'origine. Dans tous les cas on sort en temps fini du programme.

---

Preuve de propriété

On considère la propriété

I(a,q,n,r):a^q=aⁿ*r

où q est la valeur initiale de n. On montre qu'elle est toujours vraie.On remarque que la variable a est invariante . On note P(i) la propriété I précédente en fonction de l'itération i:

P(i): a^q=a^n_i*r_i

Il s'agit de vérifier que iN, P(i) est vraie. On procéde par récurrence.

Initialement, n₀=q et r₀=1 donc P(0) est vraie.

Soit iN supposons P( i). Il y a 3 cas (envisagé plus haut voir (iii)) :

n_i>0

Nous allons dans la seconde boucle. On a n_i+1=n_i-1 et r_i+1=r_i*a. On en déduit

P(i+1)=a^n_i+1*r_i+1=a^n_i-1*r_i*a=a^n_i*r_i=P(i)

Donc P(i+1) est vraie.

n_i<0

Même chose.

n_i=0

Par hypothèse de récurrence P(i) est vraie, donc a^q=a^n_i*r_i=1*r_i. Puisque n_i=0, on ne réalise aucune des 2 boucles et donc on affiche r_i=1.