Planche 1

Inf 431 -- Cours 9
Assertions et Programmes
http://jeanjacqueslevy.net
secrétariat de l'enseignement:
Catherine Bensoussan
cb@lix.polytechnique.fr
Aile 00, LIX,
01 69 33 34 67
http://www.enseignement.polytechnique.fr/informatique/IF

Planche 2

Plan

Correction de programmes itératifs scalaires
Terminaison de programmes itératifs
Correction de programmes avec des tableaux
Logique de Hoare
Récursion et assertions
Ordres bien-fondés

Planche 3

La suite de Fibonacci (1/6)

Récurrence linéaire d'ordre 2

u₀ = 0

u₁ = 1

u_n = u_n-1 + u_n-2

0, 1, 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, 144, 233, 377, 610, 987, 1597, 2584 , 4181, 6765, ...
static int fib (int n) { if (n < 2) return n; else return fib (n-1) + fib (n-2);}
ou en faisant un peu de programmation dynamique

static int fib1 (int n) { int[ ] res = new int[n+1]; res[0] = 0; res[1] = 1; for (int i=2; i <= n; ++i) res[i] = res[i-1]+res[i-2]; return res[n];}

Planche 4

La suite de Fibonacci (2/6)

ou en ne gardant que les deux dernières valeurs x et y

static int fibonacci (int n) { int x = 0; if (n != 0) { x = 1; int y = 0; for (int k=1; k != n; ++k) { int t = y; y = x; x = x + t; } } return x;}
On veut montrer que n ³ 0 =Þ x = fib(n) à la fin.

Planche 5

La suite de Fibonacci (3/6)

ou en décomposant l'instruction for.

static int fibonacci (int n) { int x = 0; if (n != 0) { x = 1; int y = 0; int k = 1; while (k != n) { int t = y; y = x; x = x + t; ++k; } } return x;}

Planche 6

La suite de Fibonacci (4/6)

static int fibonacci (int n) { //P= {n ³ 0} int x = 0; if (n != 0) { x = 1; int y = 0; int k = 1; //Q= {k £ nÙ x = fib(k)Ù y = fib(k-1)} while (k != n) { int t = y; y = x; x = x + t; ++k; } } //R= {x = fib(n)} return x;}
P assertion d'entrée
Q assertion invariant de boucle
R assertion de fin
Montrer que de P, on peut dériver R.

Planche 7

La suite de Fibonacci (5/6)

Planche 8

La suite de Fibonacci (6/6)

static int fibonacci (int n) { {n ³ 0} int x = 0; 1{n ³ 0 Ù x = 0} if (n != 0) { x = 1; int y = 0; 2{n > 0Ù x = fib(1)Ù y = fib(0)} int k = 1; {k £ nÙ x = fib(k)Ù y = fib(k-1)} while (k != n) { 3{k < nÙ x = fib(k)Ù y = fib(k-1)} int t = y; 4{k < nÙ x = fib(k)Ù y = fib(k-1) Ù t = fib(k-1) } y = x; 5{k < nÙ x = fib(k)Ù y = fib(k) Ù t = fib(k-1) } x = x + t; 6{k < nÙ x = fib(k+1)Ù y = fib(k) Ù t = fib(k-1) } ++k; } 7{k = nÙ x = fib(k)Ù y = fib(k-1)} } {x = fib(n)} return x;}

1 2 3 4 5 6 7

Planche 9

Le PGCD (1/3)

Un autre exemple itératif simple:

static int pgcd (int a, int b) { int x = a, y = b; while (x != y) if (x > y) x = x - y; else y = y - x; return x;}

Planche 10

Le PGCD (2/3)

static int pgcd (int a, int b) { {a > 0 Ù b > 0} int x = a, y = b; {x > 0 Ù y > 0 Ù pgcd(x,y) = pgcd(a,b)} while (x != y) { 2{x > 0 Ù y > 0 Ù x¹ y Ù pgcd(x,y) = pgcd(a,b)} if (x > y) { 3{x > 0 Ù y > 0 Ù x > y Ù pgcd(x-y,y) = pgcd(a,b)} x = x - y; 4{x > 0 Ù y > 0 Ù pgcd(x,y) = pgcd(a,b)} } else { 5{x > 0 Ù y > 0 Ù x < y Ù pgcd(x,y-x) = pgcd(a,b)} y = y - x; 6{x > 0 Ù y > 0 Ù pgcd(x,y) = pgcd(a,b)} } } 7{x > 0 Ù x = y = pgcd(x,y) = pgcd(a,b)} return x;}

2 3 4 5 6 7

Exercice 1 Montrer que le raisonnement n'est plus valide avec {a ³ 0 Ù b ³ 0}. Comment corriger le programme?

Planche 11

Le PGCD (3/3)

Exercice 2 Faire le raisonnement avec l'algorithme d'Euclide suivant avec {a ³ 0 Ù b ³ 0} comme assertion d'entrée.

static int pgcd (int a, int b) { int x = a, y = b; while (y != 0) { int r = x % y; x = y; y = r; } return x;}

Exercice 3 Modifier les programmes pour qu'ils acceptent comme assertion d'entrée {a Î Z Ù b Î Z}.

Planche 12

Assertions

Les variables d'un programme itératif ont des valeurs modifiables.
Une assertion est une proposition logique, décrivant une propriété d'un état mémoire des variables.
Une assertion est attachée à un point d'un programme.
Pour montrer l'implication de l'assertion de fin à partir de l'assertion d'entrée, on procède par implications successives grâce à des assertions intermédiaires.

Planche 13

Terminaison (1/2)

static int fibonacci (int n) { {n ³ 0} int x = 0; if (n != 0) { x = 1; int y = 0; int k = 1; {W(n,k) = n - k} while (k != n) { int t = y; y = x; x = x + t; ++k; } } {x = fib(n)} return x;}

En un tour de boucle comme (n,k) devient (n,k+1), on a
W(n,k) = n-k > n-k-1=W(n,k+1).

L'instruction while s'arrête donc.

Planche 14

Terminaison (2/2)

static int pgcd (int a, int b) { {a > 0 Ù b > 0} int x = a, y = b; {x > 0 Ù y>0 Ù W(x,y) = max(x,y)} while (x != y) if (x > y) x = x - y; else y = y - x; return x;}

Ici encore en un tour de boucle, si x>y, on a
W(x,y) = max(x,y) > max(x-y,y)=W(x-y,y)

De même, si x < y, on a
W(x,y) = max(x,y) > max(x,y-x)=W(x,y-x)

L'instruction while s'arrête donc.

Exercice 4 Montrer la terminaison de l'algorithme d'Euclide.

Planche 15

Assertions et tableaux (1/3)

static void drapeauHollandais (int[ ] a) { [Dijkstra] int n = a.length; int b = 0, i = 0, r = n; while (i < r) { switch (a[i]) { case BLEU: int t = a[b]; a[b] = a[i]; a[i] = t; ++b; ++i; break; case BLANC: ++i; break; case ROUGE: --r; int u = a[r]; a[r] = a[i]; a[i] = u; break; } } }

Planche 16

Assertions et tableaux (2/3)

static void drapeauHollandais (int[ ] a) { int n = a.length; int b = 0, i = 0, r = n; {f(0,b,BLEU) Ù f(b,i,BLANC) Ù f(r,n,ROUGE) Ù i £ r} while (i < r) { switch (a[i]) { case BLEU: 1{f(0,b,BLEU) Ù f(b,i,BLANC) Ù f(r,n,ROUGE) Ù a[i] = BLEU Ù i < r} int t = a[b]; a[b] = a[i]; a[i] = t; 2{f(0,b+1,BLEU) Ù f(b+1,i+1,BLANC) Ù f(r,n,ROUGE) Ù i < r} ++b; ++i; break; case BLANC: 3{f(0,b,BLEU) Ù f(b,i+1,BLANC) Ù f(r,n,ROUGE) Ù i < r } ++i; break; case ROUGE: 4{f(0,b,BLEU) Ù f(b,i,BLANC) Ù f(r,n,ROUGE) Ù a[i] = ROUGE Ù i < r} --r; 5{f(0,b,BLEU) Ù f(b,i,BLANC) Ù f(r+1,n,ROUGE) Ù a[i] = ROUGE Ù i £ r} int u = a[r]; a[r] = a[i]; a[i] = u; break; } } {f(0,b,BLEU) Ù f(b,r,BLANC) Ù f(r,n,ROUGE)} }

où f(i,j,c) = " k . i £ k < j Þ a[k] = c

1 2 3 4 5

Planche 17

Assertions et tableaux (3/3)

La terminaison du drapeau hollandais se montre en considérant l'ordinal W(b,i,r) = r - i.

Exercice 5 Montrer la correction du tri par sélection suivant:

static void triSelection (int[ ] a) { int n = a.length; for (int i = 0; i < n - 1; ++i) { int min = i; for (int j = i+1; j < n; ++j) if (a[j] < a[min]) min = j; int t = a[min]; a[min] = a[i]; a[i] = t; }}

Exercice 6 Montrer la correction du tri par insertion.

Exercice 7 Montrer la correction du tri par bulles.
(cf. cours 1ère année)

Planche 18

Quelques principes logiques

On a toujours
{P (E)} x = E; {P(x)}
Pour montrer

{P} if (E) S else S' {Q}

il faut montrer

{P Ù E} S {Q}

et

{P Ù ¬ E} S' {Q}
Pour montrer

{P} while (E) S {Q}

il faut deviner l'invariant I, et montrer P Þ I et I Ù ¬ E Þ Q et
{I Ù E} S {I}

cf. logique de Floyd-Hoare.
Dans le triplet {P} S {Q}, on appelle P et Q des pré-condition et post-condition de S.

Planche 19

Logique de Hoare

{P (E)} x = E; {P(x)}

{P Ù E} S {Q} {P Ù ¬ E} S'{Q}

{P} if (E) S else S' {Q}

{P} S {Q} {Q} S'{R}

{P} S S'{R}

{P} S {Q}

{P} {S} {Q}

{P Ù E} S {P}

{P} while (E) S {P Ù ¬ E}

P Þ P' {P'} S {Q'} Q' Þ Q

{P} S {Q}

Les formules sont des triplets {P} S {Q}.

Les prémisses d'une règle d'inférence sont au dessus de la barre.

La conclusion d'une règle d'inférence est en dessous.

Un axiome est une règle sans prémisse.

Planche 20

Correction partielle -- Correction totale

{P} S {Q} vrai montre que si P est vrai, alors Q l'est aussi. Tout dépend donc de ce qu'on veut prouver avec Q. Par exemple, on peut ne s'intéresser qu'à la valeur d'une seule variable, sans se soucier du reste.
{P} S {Q} vrai ne donne aucune indication de terminaison, puisque Q n'est vrai que si S termine. On dit qu'il y a correction partielle.
seuls des ordinaux W qui décroissent dans les boucles assurent la terminaison. Alors on a correction totale.
assertions ¹ spécifications. Faire la correspondance entre spécifications (le cahier des charges) et programmes est plus complexe et souvent imprécis.
la correspondance entre spécifications et programmes peut se faire progressivement: programmation par raffinements successifs (stepwise refinement).
les spécifications sont parfois formelles (B, TLA, Coq, Isabelle, HOL, PVS, etc); on peut alors formaliser la correspondance entre spécifications et programmes (méthodes formelles ).

Planche 21

Implémentation des assertions (1/2)

Java 1.4: l'instruction assert lève AssertionError si l'assertion n'est pas vérifiée. Beaucoup de langages ont cette facilité: Caml, C, C++.

int n = a.length; int b = 0, i = 0, r = n; assert phi(a,0,b,BLEU) && phi(a,b,i,BLANC) && phi(a,r,n,ROUGE) && i <= r; while (i < r) { switch (a[i]) { ... } assert phi(a,0,b,BLEU) && phi(a,b,i,BLANC) && phi(a,r,n,ROUGE); } assert phi(a,0,b,BLEU) && phi(a,b,r,BLANC) && phi(a,r,n,ROUGE); } static boolean phi (int[ ] a, int i, int j, int c) { return i >= j || a[i] == c && phi(a, i+1, j, c); }
javac -source 1.4 DutchFlag.java
java -enableassertions DutchFlag 0 12

Planche 22

Implémentation des assertions (2/2)

On peut l'implémenter en Java 1.1.8 par:

class AssertionError extends Error { }public class Assertion { public static void check (boolean e) { if (!e) throw new AssertionError(); }}
On peut passer en argument de Assertion.check une expression booléenne quelconque correspondant à l'assertion à tester.
Bien sûr, les assertions avec des quantificateurs " ou $ sont plus dures à tester!

Planche 23

Récursion et assertions (1/3)

On veut montrer {n ³ 0} r = fact(n); {fact(n) = n!}

Pour cela, on suppose (comme pour les boucles) que les appels (récursifs) utilisés vérifient déjà cette formule.
static int fact (int n) { int r; {n ³ 0 Ù " n fact(n) = n! } if (n == 0) { 1{n = 0 } r = 1; 2{n = 0 Ù r = 1 = 0!} } else { 3{n-1 ³ 0 Ù fact(n-1) = (n-1)!} r = n * fact(n-1); 4{r = n (n-1)! = n!} } {r = n!} return r;}

1 2 3 4
A nouveau, il s'agit de correction partielle.
Un autre argument montre la terminaison.

Planche 24

Récursion et assertions (2/3)

On veut montrer {n ³ 0} r = f(n); {f(n) = ifn > 100 then n-10 else 91}
static int f (int n) { // ------------------ fonction 91 [McCarthy] int r; {n ³ 0 Ù " n' f(n') = ifn' > 100 then n'-10 else 91} if (n > 100) { 1{n > 100} r = n-10; 2{n > 100 Ù r = n-10 } } else { 3{n £ 100 Ù " n' f(n') = ifn' > 100 then n'-10 else 91} r = f(f(n+11)); 4{n £ 100 Ù r = F(n)} «5{n £ 100 Ù r = 91} } {r = ifn > 100 then n-10 else 91} return r;}

4

F(n) = f(ifn+11 > 100 then n+1 else 91)

= ifn ³ 90 then f(n+1) else f(91)

= ifn ³ 90 then ifn ³ 100 then n-9 else 91 else 91

= ifn ³ 100 then n-9 else 91

1 2 3 4 5

Planche 25

Récursion et assertions (3/3)

Considérons l'insertion dans une liste triée

\shell{10}{bigrxvt}{-geometry 70x10+150+700}{{\tiny Exécution}} static Liste inserer (int x, Liste a) { int r; if (a == null || x < a.val) { r = new Liste(x, a); } else if (a.val < x) { r = new Liste(a.val, inserer(x, a.suiv)); } else r = a; return r;}
Considérons les propositions
{ord(a) = (a = null Ú a.suiv = null Ú a.val < a.suiv.val Ù ord(a.suiv))}
On cherche à montrer

{ord(a)} r = inserer(x,a); {ord(inserer(x,a))}

Exercice 8 Le démontrer... Indication: se servir de la formule

{prem(x,a) = (a = null Ú inserer(x,a).val = x Ú inserer(x,a).val = a.val)}

Planche 26

Ordres bien-fondés et terminaison (1/3)

Une relation d'ordre (strict) est une relation:

irréflexive x ¬ x

transitive x y z Þ x z
Un ordre bien fondé est une relation d'ordre qui n'admet pas de chaîne infinie descendante x₀ x₁ x₂ ··· x_n ···.
Exemples d'ordre bien fondés
·á N, < ñ
·ordre lexicographique: á N×N, <_lex ñ

(x, y) <_lex (x',y')
ssi

x<x' Ú (x=x' Ù y<y')

(4,3) >_lex (4,2) >_lex (3,15) >_lex (3, 6) >_lex (3,4) >_lex (3,2) >_lex (2, 21) >_lex (2, 19) >_lex (2, 12) >_lex (1, 90) ...
·ordre des multi-ensembles: á P(N), <_mul ñ

E <_mul E'
ssi

E = F È {y₁, y₂, ... y_n}, E' = F È {x} (y_i < x, n ³ 0)

{4, 5, 5 } >_mul {3, 5, 5 } >_mul {3, 4, 4, 4, 5 } >_mul {3, 4, 4, 5 } >_mul {3, 2, 2, 2, 1, 4, 5 } >_mul {3, 1, 0, 2, 2, 1, 4, 5 } >_mul {3, 1, 4, 5 } >_mul ...

Planche 27

Ordres bien-fondés et terminaison (2/3)

·ordre de simplication: á A(N), ñ
A(N) arbres étiquetés par des entiers naturels

t=n(t₁, t₂, ··· t_n) u=m(u₁, u₂, ··· u_p) si n > m et t u₁, t u₂, ··· t u_p

t=n(···, t_i, ···) u=n(···, ···)

Théorie des w.q.o. (well quasi orderings) [Kruskal, Nash-Williams, Plaisted, Dershowitz]
Théorie des systèmes de réécriture
Démonstration automatique.

En fait tout ordre sur les arbres étiquetés par un ensemble fini E Ì N vérifiant:

	t=n(t₁, t₂, ··· t_n) u=n(u₁, u₂, ··· u_p) si t_i u_i pour un i
	t=n(···, t_i, ···) u=n(···, ···)

est bien fondé.

Planche 28

Ordres bien-fondés et terminaison (3/3)

Exercice 9 Trouver les ordres bien-fondés qui permettent de conclure à la terminaison de ces deux fonctions récursives (fonction 91 de [McCarthy] ou de [Ackermann]).

static int ack (int m, int n) { if (m == 0) return n + 1; else if (n == 0) return ack (m - 1, 1); else return ack (m - 1, ack (m, n - 1));}

Indications: considérer l'ordre lexicographique pour Ackermann et l'ordre partiel suivant pour 91:

0 1 2 ··· 98 99 100 x

où x quelconque tel que x > 100.

Planche 29

Exercices

Exercice 10 Montrer la correction de Quicksort.

Exercice 11 Montrer la correction de la fusion de listes triées.

Exercice 12 Montrer la correction du test d'acyclicité des graphes par depth-first-search.

Exercice 13 Montrer que la terminaison peut être une propriété aussi dure à montrer que la correction.

This document was translated from L^AT_EX by H^EV^EA.

F(n)	=	f(ifn+11 > 100 *then* n+1 *else* 91)
	=	ifn ³ 90 *then* f(n+1) *else* f(91)
	=	ifn ³ 90 *then* ifn ³ 100 *then* n-9 *else* 91 *else* 91
	=	ifn ³ 100 *then* n-9 *else* 91

	t=n(t₁, t₂, ··· t_n) u=m(u₁, u₂, ··· u_p) si n > m et t u₁, t u₂, ··· t u_p
	t=n(···, t_i, ···) u=n(···, ···)