Théorie des langages : Tp 1 redimensionnement d'un tableau
Télécharger PDFPreuve de Correction Partielle de Programme
Exercice 1 : Redimensionnement d’un tableau
Pour réduire la consommation mémoire, on utilise souvent en programmation des tableaux dynamiques qui ajustent leur taille en multipliant ou divisant par 2 le nombre de données qu’ils contiennent. L’implémentation des tableaux dynamiques repose sur des tableaux de taille fixe qu’on redimensionne en les tronquant ou en les recopiant dans un tableau de taille double lorsque les limites sont atteintes. Il a été démontré que le facteur 2 offre la meilleure complexité amortie, c’est-à-dire que sur une utilisation suffisamment intense du tableau, le temps de recopie devient négligeable et l’accès aux données est quasi immédiat, comme dans un tableau de taille fixe.
Le but de cet exercice est de prouver la correction partielle de l’algorithme suivant de redimensionnement d’un tableau T[0..N−1] de taille N en un tableau D[0..2N−1] de taille double.
programme
0 i := 0 ;
1 while (i < N) {
2 D[N + i] := 0 ;
3 D[i] := T[i] ;
4 i := i + 1 }
5 r := N + i
Q1 : Compléter le tableau D
T = [4, 7, 2, 8]
N = 4
D = [4, 7, 2, 8, 0, 0, 0, 0]
Q2 : Automate correspondant au programme
q0 → q1 (i := 0)
q1 → q2 (test : i < N)
q2 → q3 (affectation : D[N + i] := 0)
q3 → q4 (affectation : D[i] := T[i])
q4 → q1 (affectation : i := i + 1)
q1 → q5 (test : i ≥ N)
q5 → qs (affectation : r := N + i)
Q3 : Propriété ψs
ψs = { r = 2N, ∀k ∈ [0..N−1], D[k] = T[k], ∀` ∈ [N..2N−1], D[`] = 0 }
Q4 : Preuve de correction
Transition q5 → qs (affectation : r := N + i)
ψ5 = ψs [r ← N + i] ≡ { N + i = 2N, ∀k ∈ [0..N−1], D[k] = T[k], ∀` ∈ [N..2N−1], D[`] = 0, i = N } ≡ { ∀k ∈ [0..i−1], D[k] = T[k], ∀` ∈ [N..N + i−1], D[`] = 0, i = N }
Transition q1 → q2 (test : i < N)
ψ2 = { ∀k ∈ [0..i−1], D[k] = T[k], ∀` ∈ [N..N + i−1], D[`] = 0, i + 1 ≤ N }
Transition q4 → q1 (affectation : i := i + 1)
ψ4 = ψ1 [i ← i + 1] ≡ { ∀k ∈ [0..i], D[k] = T[k], ∀` ∈ [N..N + i], D[`] = 0, i + 1 ≤ N }
Transition q3 → q4 (affectation : D[i] := T[i])
ψ3 = ψ4 [D[i] ← T[i]] ≡ { (∀k ∈ [0..i−1], D[k] = T[k]) ∧ D[i] = T[i], ∀` ∈ [N..N + i], D[`] = 0, i + 1 ≤ N } ≡ { ∀k ∈ [0..i−1], D[k] = T[k], ∀` ∈ [N..N + i−1], D[`] = 0 }
Transition q2 → q3 (affectation : D[N + i] := 0)
ψ2 = { ∀k ∈ [0..i−1], D[k] = T[k], (∀` ∈ [N..N + i−1], D[`] = 0) ∧ D[N + i] = 0, i + 1 ≤ N } ≡ { ∀k ∈ [0..i−1], D[k] = T[k], ∀` ∈ [N..N + i−1], D[`] = 0, i + 1 ≤ N }
Vérification de l’invariant
Pour la transition q1 → q2 (test : i < N), on vérifie que ψ1 ∧ i < N ⇒ ψ2.
Les propriétés quantifiées sont identiques, et i + 1 ≤ N est une conséquence directe de i < N et i entier.
Q5 : Conditions d’utilisation
Les conditions d’utilisation du programme sont : N ≥ 0.
FAQ
1. Qu’est-ce qu’un tableau dynamique ?
Un tableau dynamique est une structure de données qui ajuste automatiquement sa taille en fonction du nombre d’éléments stockés, souvent par multiplication ou division par 2.
2. Pourquoi le facteur 2 est-il optimal pour le redimensionnement ?
Le facteur 2 offre la meilleure complexité amortie, car il réduit le nombre d’opérations de recopie nécessaires pour maintenir une efficacité proche d’un tableau de taille fixe.
3. À quoi sert la preuve de correction partielle ?
Elle permet de vérifier que l’algorithme produit un résultat correct pour certaines conditions d’entrée, sans garantir que toutes les conditions possibles sont couvertes.
Exercice 2 : Multiplication rapide
Le but de cet exercice est de démontrer la correction partielle de l’algorithme suivant de multiplication rapide.
programme
0 x := A ; y := B ; r := 0 ;
1 while (y > 0) {
2 if (y mod 2 ? = 0) {
3 x := x + x ; y := y ÷ 2
4 } else {
5 r := r + x ; y := y − 1
6 }
7 }
Q6 : Automate correspondant au programme
q0 → q1 (x := A ; y := B ; r := 0)
q1 → q2 (test : y > 0)
q2 → q3 (test : y mod 2 = 0)
q3 → q1 (affectation : x := x + x ; y := y ÷ 2)
q2 → q5 (test : y mod 2 ≠ 0)
q5 → q1 (affectation : r := r + x ; y := y − 1)
q1 → qs (test : y ≤ 0)
Q7 : Exécution état par état pour A = 3 et B = 5
q0 : x = 3, y = 5, r = 0
q1 : x = 3, y = 5, r = 0
q2 : x = 3, y = 5, r = 0
q5 : x = 3, y = 5, r = 0 → r = 0 + 3 = 3, y = 4
q1 : x = 3, y = 4, r = 3
q2 : x = 3, y = 4, r = 3
q3 : x = 3, y = 4, r = 3 → x = 6, y = 2
q1 : x = 6, y = 2, r = 3
q2 : x = 6, y = 2, r = 3
q3 : x = 6, y = 2, r = 3 → x = 12, y = 1
q1 : x = 12, y = 1, r = 3
q2 : x = 12, y = 1, r = 3
q5 : x = 12, y = 1, r = 3 → r = 3 + 12 = 15, y = 0
qs : x = 12, y = 0, r = 15
Q8 : Question de cours
Un invariant ψ de l’état q signifie que la propriété ψ reste vraie à chaque passage par l’état q, avant et après l’exécution de la transition correspondante.
Q9 : Propriété de correction
ψs = { r = A × B, y = 0 }
Q10 : Preuve de correction
Transition q1 → qs (test : y ≤ 0)
ψ1 = { r + x × y = A × B, y ≥ 0 }
Preuve : y ≤ 0 et y ≥ 0 ⇒ y = 0. Donc r = A × B.
Transition q5 → q1 (affectation : r := r + x ; y := y − 1)
ψ5 = ψ1 [r ← r + x ; y ← y − 1] ≡ { r + x + x × (y − 1) = A × B, y − 1 ≥ 0 } ≡ { r + x × y = A × B, y ≥ 0 }
Transition q3 → q1 (affectation : x := x + x ; y := y ÷ 2)
ψ3 = ψ1 [x ← x + x ; y ← y ÷ 2] ≡ { r + (x + x) × (y ÷ 2) = A × B, y ÷ 2 ≥ 0 }
Preuve : (x + x) × (y ÷ 2) = x × y, donc r + x × y = A × B.
Transition q2 → q3 (test : y mod 2 = 0)
ψ2 = { r + x × y = A × B, y ≥ 0 }
Preuve : y mod 2 = 0 ⇒ y est pair. Donc (x + x) × (y ÷ 2) = x × y.
Transition q2 → q5 (test : y mod 2 ≠ 0)
ψ2 ∧ y mod 2 ≠ 0 ⇒ ψ5
Preuve : y mod 2 ≠ 0 ⇒ y est impair et y ≥ 1. Donc y − 1 ≥ 0.
Transition q1 → q2 (test : y > 0)
ψ1 ∧ y > 0 ⇒ ψ2
Preuve : ψ1 et ψ2 sont identiques.
Q11 : Conditions d’utilisation
Les conditions d’utilisation du programme sont : B ≥ 0.
FAQ
1. Qu’est-ce que la multiplication rapide ?
La multiplication rapide est une méthode algorithmique qui calcule le produit de deux nombres en utilisant des opérations de décalage et d’addition pour optimiser les calculs.
2. Pourquoi l’algorithme utilise-t-il y mod 2 ?
L’opération y mod 2 permet de déterminer si y est pair ou impair, ce qui guide l’algorithme vers la bonne branche (décalage ou addition).
3. À quoi sert la propriété r + x × y = A × B ?
Cette propriété exprime que la valeur de r accumulée, combinée avec x × y, correspond toujours au produit final A × B à chaque étape de l’algorithme.