Théorie des langages : Tp 1 redimensionnement d'un tableau
Télécharger PDFPreuve de Correction Partielle de Programme
Exercice 1Redimensionnement d’un tableau(30 min) (9 pt)
Afin de réduire la consommation mémoire on utilise fréquemment en programmation, les
tables dynamiquesqui s’ajustent aux nombres de données qu’ils contiennent en multipliant
(ou en divisant) leur taille par 2. L’implantation des tables dynamiques utilise destableaux
de taille fixeet les 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 un utilisation suffisament 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 redimensionne-
ment d’un tableauT[0..N−1]de tailleNen un tableauD[0..2N−1]de taille double.
programme
0i := 0 ;
1while(i<N){
2D[N+i] := 0;
3D[i] := T[i] ;
4i := i + 1 }
5r :=N+ i
Q1.(0.25 pt)Complétez le tableauDobtenu après exécution du programme précédent sur le tableauT= k0123
T[k]4728
de tailleN= 4.
`01234567
D[`]47280000
Q2.(1 pt)Donnez l’automate correspondant au programme.q 0i:=0 −−−→q1 q1 i<N−−−−→q 2
D[N+i]:=0
−−−−−−−→q3 q3 D[i]:=T[i]
−−−−−−→q4 i:=i+1−−−−−→q 1q 1i≥N −−−−→q5 r:=N+i
−−−−−−→qs Q3.(0.75 pt)Complétez la propriétéψs associée à l’état de sortieqs du programme de manière à
exprimer
— quercorrespond au double de la taille du tableauT
— que le tableauTest recopié en première partie deD
— que la seconde partie deDcontient uniquement des0
— d’autres propriétés que vous jugerez utiles pour prouver les précédentesψ sdef = r= 2N
∀k∈[0..N−1],D[k] =T[k]
∀`∈[N..2N−1],D[`] = 0i=N Q4. Preuve de correction(6 pt)Montrez par la méthode de Floyd-Dijkstra-Hoare vue en cours
qu’à la sortie du programme la propriétéψs est vérifiée :
Indication :
1. Vous indiquerez toujours la transition considérée et vous prendrez soin de rédiger complètement
une transition test, une transition d’affectation et une transition de vérification.
2. Pour effectuer correctement les affectations en arrière vous aurez besoin de réécrire les∀sous une
forme qui fait apparaître explicitement le terme que vous devez substituer.
Par exemple,( ∀x∈[a..b],Propriété(x)) ≡Propriété(a)∧( ∀x∈[a+ 1..b−1],Propriété(x)) ∧Propriété(b)
solution ψ 5
(1 pt)À partir de la propriétéψs , on détermine la propriétéψ5 grâce à la transitionq5 r:=2∗i−−−−−→ affect.q s
. Cette
transition fait uniquement des affectations donc le meilleur choix pourψ5 est :ψ 5def =ψs [r←N+i]≡ N+i= 2N
∀k∈[0..N−1],D[k] =T[k]
∀`∈[N..2N−1],D[`] = 0i=N ≡
∀k∈[0..i−1],D[k] =T[k]
∀`∈[N..N+i−1],D[`] = 0i=N ψ 1
(1 pt)À partir de la propriétéψ5 , on détermine la propriétéψ1 grâce à la transitionq1 i≥N−−−−→ testq 5
. Cette
transition effectue un test, elle doit donc satisfaire l’implication suivante :ψ 1∧i≥N ︸︷︷︸ test? =⇒ψ5 On choisit de prendreψ 1:
∀k∈[0..i−1],D[k] =T[k]
∀`∈[N..N+i−1],D[`] = 0i≤N Montrons que ce choix deψ1 satisfait l’implication
—i≤Net le test donnei=N
— on peut donc remplaceriparNdans les intervalles des propriétés quantifiées pour obtenir
∀k∈[0..N−1],D[k] =T[k]et∀`∈[N..2N−1],D[`] = 0
Ce qui conclut la preuve de l’implicationψ1 ∧i≥N=⇒ψ5 ψ4 (1 pt)On détermineψ4 grâce à la transitionq4 i:=i+1−−−−−→ affect.q 1. ψ4 def=ψ 1
[i←i+ 1]≡ ∀k∈[0..i+ 1−1],D[k] =T[k]
∀`∈[N..N+i+ 1−1],D[`] = 0
i+ 1≤N ≡ ∀k∈[0..i],D[k] =T[k]
∀`∈[N..N+i],D[`] = 0
i+ 1≤N ψ3 (1 pt)On détermineψ3 grâce à la transitionq3 D[i]:=T[i]−−−−−−→ affect.q 4ψ 3def =ψ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 [D[i] :=T[i]]≡ ( ∀k∈[0..i−1],D[k] =T[k]) ∧T[i] =T[i]
∀`∈[N..N+i],D[`] = 0
i+ 1≤N ≡ ∀k∈[0..i−1],D[k] =T[k]
∀`∈[N..N+i],D[`] = 0
i+ 1≤N ψ2 (1 pt)On détermineψ2 grâce à la transitionq2 D[N+i]:=0
−−−−−−−→affect. q3 ψ2 def=ψ 3
[D[N+i] := 0]≡
∀k∈[0..i−1],D[k] =T[k]( ∀`∈[N..N+i−1],D[`] = 0) ∧D[N+i] = 0
i+ 1≤N [D[N+i] := 0]≡
∀k∈[0..i−1],D[k] =T[k]( ∀`∈[N..N+i−1],D[`] = 0) ∧0 = 0
i+ 1≤N ≡ ∀k∈[0..i−1],D[k] =T[k]
∀`∈[N..N+i−1],D[`] = 0
i+ 1≤N � vérification(1 pt)Les propriétésψ1 etψ2 étant choisies. On utilise la transitionq1 i<N−−−−→ testq 2
pour vérifier que les
propriétés que nous avons choisies sont bien des invariants. La transition effectue un test, elle doit donc
satisfaire l’implication : ∀k∈[0..i−1],D[k] =T[k]( ∀`∈[N..N+i−1],D[`] = 0) i≤N :ψ1 ∧i< N︸︷︷︸ test? =⇒ψ2 : ∀k∈[0..i−1],D[k] =T[k]
∀`∈[N..N+i−1],D[`] = 0
i+ 1≤N Les propriétés quantifiées sont identiques de chaque côté de l’implication. Donc il reste uniquement à
montreri+ 1≤Nqui est une conséquence du testi< Net du fait queiest un entier.
L’implication est valide et nos propriétés sont donc des invariants.
Q5. Conditions d’utilisation(1 pt)En déduire les conditions d’utilisation du programme.
solution
On détermine les conditions d’utilisation (propriétéψ0 ) grâce à la transitionq0 i:=0−−−→ affect.q 1. ψ0 def=ψ 1[i←0]≡
∀k∈[0..−1],D[k] =T[k]( ∀`∈[N..N−1],D[`] = 0) 0≤N ≡0≤N
Les intervalles[0..−1]et[N..N−1]sont vides, donc les propriétés∀k∈∅, ...et∀`∈∅, ...sont trivialement
satisfaites.
Conclusion : la contrainte d’utilisation se réduit àN≥0.
Exercice 2Multiplication rapide(30 min) (11 pt)
Le but de l’exercice est de démontrer la correction partielle de l’algorithme suivant de multiplicationrapide. programme
0x:=A ; y:=B ; r:=0 ;
1while(y>0){
2if (ymod2? = 0){
3x := x+x ; y := y÷2
4} else {
5r := r+x ; y := y-16} 7}
Q6.(1 pt)Donnez l’automate correspondant au programme.
solutionq 0
x:=A;y:=B;r:=0
−−−−−−−−−−−−−−→q1 q1 y>0−−−→q 2ymod2=0 −−−−−−−→q3 x:=x+x;y:=y÷2
−−−−−−−−−−−−→q1 q2 ymod26=0
−−−−−−−→q5 r:=r+x;y:=y−1
−−−−−−−−−−−−→q1 q1 y≤0−−−→q s
Q7.(1 pt)Poursuivez sur votre copie l’exécution état par état de l’automate précédent dans le cas
A= 3,B= 5
solutionétatxyr q0 ???q 1350 y >0q 2350 ymod26= 0q 5350 q1 343
y >0q 2343 ymod2 = 0q 3343 q1 623
y >0q 2623 ymod2 = 0q 3623 q1 1213
y >0q 21213 ymod26= 0q 51213 q1 12015y≤0 qs 12015
Q8. Question de cours(1 pt)Expliquez en quelques phrases ce que signifie « la propriétéψest
un invariant de l’étatq».
Q9.(1 pt)Donnez la propriété de correction qui exprime qu’à la sortie de ce programmercontient
la valeur deA×B.
solutionψ sdef ={ r=A×B
y= 0} Q10. Preuve de correction(6 pt)Montrez par la méthode de Floyd-Dijkstra-Hoare vue en cours
qu’à la sortie du programme la propriétéψs est vérifiée.
Indication :Vous indiquerez toujours la transition considérée et vous prendrez soin de rédiger com-
plètement une transition test, une transition d’affectation et une transition de vérification.
Q11. Conditions d’utilisation(1 pt)Donnez les conditions d’utilisation du programme.
solution ψ 1
(1 pt)À partir de la propriétéψs , on détermine la propriétéψ1 grâce à la transitionq1 y≤0−−−→ testq s
. Cette
transition effectue un test, elle doit donc satisfaire l’implication suivante :ψ 1∧y≤0 ︸︷︷︸test ?=⇒ψ s
On choisit de prendreψ 1def ={ r+x×y=A×B(†)y≥0(‡) Montrons que ce choix deψ1 satisfait l’implication
Preuve(‡)et le test impliquey= 0 (X). On peut donc remplacerypar 0 dans(†)pour obtenir
r=A×B(X). Ceci montre queψs est bien une conséquence du membre gauche de l’implication. ψ 5
(1 pt)À partir de la propriétéψ1 , on détermine la propriétéψ5 grâce à la transitionq5 r:=r+x;y:=y−1
−−−−−−−−−−−−→affect. q1 .
Cette transition fait uniquement des affectations donc le meilleur choix pourψ5 est :ψ 5def =ψ1 [r←r+x;y←y−1]≡{ r+x+x×(y−1) =A×By−1≥0 }≡ {
r+x×y=A×By−1≥0 } ψ 3
(1 pt)À partir de la propriétéψ1 , on détermine la propriétéψ3 grâce à la transitionq3 x:=x+x;y:=y÷2
−−−−−−−−−−−−→affect. q1 .
Cette transition fait uniquement des affectations donc le meilleur choix pourψ3 est :ψ 3def =ψ1 [x←x+x;y:=y÷2]≡{ r+ (x+x)×(y÷2) =A×By÷2≥0 } ψ 2
(1 pt)À partir de la propriétéψ3 , on détermine la propriétéψ2 grâce à la transitionq2 ymod2=0
−−−−−−−→test q3 .
Cette transition effectue un test, elle doit donc satisfaire l’implication suivante :ψ 2
∧ymod2 = 0︸ ︷︷︸test ?=⇒ψ 3
On choisit de prendreψ 2def ={ r+x×y=A×B(†)y≥0(‡) Montrons que ce choix deψ2 satisfait l’implicationPreuve 1.(‡)impliquey÷2≥0 (X).
2. Remarquons quex+x=x×2et donc(x+x)×(y÷2) =x×2×(y÷2)Par ailleurs, le
test implique queyest pair et donc2×(y÷2) =y. Finalement,(x+x)×(y÷2) =x×y
et donc(†)impliquer+ (x+x)×(y÷2) =A×B(X).
Ceci montre queψ3 est bien une conséquence du membre gauche de l’implication. �
Vérification 1(1 pt)Les propriétésψ2 etψ5 étant choisies. On utilise la transitionq2 ymod26=0
−−−−−−−→test q5 pour vérifier que les
propriétés que nous avons choisies sont bien des invariants. La transition effectue un test, elle doit donc
satisfaire l’implication :{ (†)r+x×y=A×B(‡)y≥0 }:ψ 2
∧ymod26= 0︸ ︷︷︸test ⇒ψ5 :{ r+x×y=A×B(X)d’après(†)y−1≥0 }
PreuveIl reste uniquement à montrer quey−1≥0, autrement dit quey≥1. D’après le test,
yest impair et d’après(‡)y≥0or le premier nombre impair positif est 1 doncy≥1 (X). Ceci
prouve la validité de l’implication. �
Vérification 2(1 pt)Les propriétésψ1 etψ2 étant choisies. On utilise la transitionq1 y>0−−−→ testq 2
pour vérifier que les
propriétés que nous avons choisies sont bien des invariants. La transition effectue un test, elle doit donc
satisfaire l’implication :ψ 1
∧y >0︸ ︷︷︸test ⇒ψ2 PreuveL’implication est trivialement satisfaite puisqueψ1 etψ2 sont identiques. ψ 0
(1 pt)On détermine les conditions d’utilisation (propriétéψ0 ) grâce à la transitionq0 x:=A;y:=B;r:=0
−−−−−−−−−−−−−−→affect. q1 .ψ 0def =ψ1 [x←A;y←B;r←0]≡{ r+x×y=A×By≥0 }
[x←A;y←B;r←0]≡ {
0 +A×B=A×BB≥0 }
≡B≥0