Théorie des langages : Sujet automate et grammaires
Télécharger PDFAutomate & Grammairespolytech’ grenoble/ricm3
nom. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Prénom . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
RICM3 – Automates et Grammaires
Durée : 1h00, sans documents.
— Tous les appareils électroniques sont interdits à l’exception des montres, et encore,
à condition qu’elles ne communiquent pas.
— Le barème est donné à titre indicatif.
— Le sujet est sur 20 points et comporte 2 exercices indépendants.
SUJET A
Exercice 1Fonctions tabulées en bijection(11 pt)
Un tableauG[0..N−1]permet de représenter une fonctiongdéfinie sur[0..N−1]. Il suffit de placer
dans la casekdu tableauGla valeur de la fonctiongenk.
Exemple :Considéronsg(k) = (k+ 2)modN. Le tableauGcontient les valeurs précalculées deg.
k01234...k...N−2N−1
G[k]23456...g(k)...01
En pratique on utilise la technique des fonctions tabulées pour calculer rapidementsin,sin−1 ,...au
moyen de tableaux préremplissin, sin- inv,....
Dans cet exercice on considère des fonctionsgetfde[0..N−1]→[0..N−1], tabulées respectivement
dans les tableauxGetF. On aimerait déterminer sigetfforment une bijection, c’est-à-dire si
∀k∈[0..N−1], g(f(k)) =k.Avec les versions tabuléesGetFdes fonctions, cela devient
GetFforment une bijection si
∀k∈[0..N−1], G[F[k]] =k
Q1.(0.5 pt)Complétez le tableauFde sorte queGetFforment une bijection :k 01234
G[k]23401k01234 F[k]34012
On considère le programme suivant qui prend en entrée deux tableauxG[0..N]etF[0..N]déjà remplis
et qui répond vrai si les tableaux sont en bijection et faux sinon.
programme
1j:= 0 ;
2while(j < N){
3if ( G[F[j]]6=j)
4then { return false }
5else { j:=j+1 }6} 7return true
M.PérinUniversité Grenoble-Alpes1
Automate & Grammairespolytech’ grenoble/ricm3
Q2. Automate(1 pt)Complétez les transitions de l’automate correspondant au programme
Indication :On rappelle que l’instruction «return valeur» se traduit par une transition vers l’état
de sortie portant une affectation «result := valeur».q 0j:=0 −−−→q1 j≥N−−−→q 2
result:=true
−−−−−−−−→qs q1 j<N−−−→q 3G[F[j]] ?=j −−−−−−−→q4 j:=j+1−−−−−→q 1q 3
G[F[j]]6=j
−−−−−−−→q5 result:=f alse
−−−−−−−−−→qs Q3. Propriété de correction(0.5 pt)Complétez la propriétéψs qui caractérise le fait que le
résultat du programme indiquesiGetFforment une bijection.ψ s: {
result=true=⇒( ∀k∈[0..N−1], G[F[k]] =k) result=false=⇒( ∃k∈[0..N−1], G[F[k]]6=k) Indication :Inspirez vous de la propriété de correction de l’algorithme de recherche par dichotomie,
vue en cours.
Q4. Preuve de correction(8 pt)Montrez par la méthode de Floyd-Dijkstra-Hoare qu’à la sortie
du programme la propriétéψs est vérifiée.
Indication :
1. Vous indiquerez toujours la transition considérée. Vous prendrez soin de rédiger complétement une
transition testet unetransition affectation,la vérification et sa conclusion.
2. Vous aurez besoin de réécrire les∀sous une forme qui fait apparaître explicitement le terme qui
vous intéresse. Aidez vous de l’équivalence
∀k∈[a..b],propriété(k)équivaut à( ∀k∈[a..b−1],propriété(k)) ∧
propriété(b)
3. On vous conseille de déterminer les invariants dans l’ordre suivant :ψ2 ,ψ1 ,ψ4 ,ψ3 ,ψ5 4. Vous prendrez comme invariant enq1 une propriété de la formeψ 1: {j≤N ∀k∈[0..j−1], G[F[k]] =k
solution ψ 2
(1 pt)À partir de la propriétéψs , on détermine la propriétéψ2 grâce à la transitionq2 result:=true
−−−−−−−−−→
affectationq s. Cette transition fait uniquement des affectations donc le meilleur choix pourψ2 est :ψ 2def =ψs [ � result← � true]≡ { �
result=true=⇒( ∀k∈[0..N−1], G[F[k]] =k) � result=false=⇒( ∃k∈[0..N−1], G[F[k]]6=k) }[ � result← � true] ≡{ � true=true=⇒( ∀k∈[0..N−1], G[F[k]] =k) � true=false=⇒( ∃k∈[0..N−1], G[F[k]]6=k) ≡ ∀k∈[0..N−1], G[F[k]] =k ψ 1
(1 pt)À partir de la propriétépsi2 on détermine la propriétéψ1 grâce à la transitionq1 j≥N−−−−→ testq 2
. Cette
transition effectue un test, elle doit donc satisfaire l’implication suivante :ψ 1∧j≥N ︸︷︷︸ test? =⇒ψ2 On choisit de prendreψ 1: { j≤N ∀k∈[ � 0.. j−1 ], G[F[k]] =k
Montrons que ce choix deψ2 satisfait l’implicationψ 1
et le testj≥Nimpliquej=Nqui avec la seconde propriété deψ1 donneψ2 Ce qui conclut la preuve de l’implicationψ1 ∧j≥N=⇒ψ2 M.PérinUniversité Grenoble-Alpes2
Automate & Grammairespolytech’ grenoble/ricm3 ψ 4
(1 pt)On détermineψ4 grâce à la transitionq4 j:=j+1−−−−−→ affectationq 1ψ 4def =ψ1 [j←j+ 1]≡ { j≤N ∀k∈[ � 0.. j−1 ], G[F[k]] =k} [j←j+ 1]≡ {
j+ 1≤N∀k∈[ � 0.. �
j], G[F[k]] =k ψ 3
(1 pt)On détermineψ3 grâce à la transitionq3 G[F[j]]? =j
−−−−−−−→test q4 Cette transition effectue un test, elle doit
donc satisfaire l’implication suivante :ψ 3
∧G[F[j]]? =j︸︷︷︸ test? =⇒ψ4 Remarquons queψ4 peut s’écrireψ 4≡ {
j+ 1≤N
G[F[j]] =j∧ (∀k∈[ � 0..
j−1 ], G[F[k]] =k) On choisit donc de prendreψ 3def ={ j+ 1≤N∀k∈[ � 0..
j−1 ], G[F[k]] =k
et l’implicationψ3 ∧G[F[j]] =j? =⇒ψ4 est satisfaite. �
vérification 1(1 pt)Les propriétésψ2 etψ3 étant choisies, on utilise la transitionq1 j<N−−−−→ testq 3
pour vérifier que les
propriétés que nous avons choisies sont bien des invariants. Cette transition effectue un test, elle doit
donc satisfaire l’implication suivante :ψ 1
∧j < N︸︷︷︸ test? =⇒ψ3 ψ1 def= { j≤N ∀k∈[ � 0.. j−1 ], G[F[k]] =k} ?=⇒ ok=⇒ ψ3 def= {
j+ 1≤N∀k∈[ � 0..
j−1 ], G[F[k]] =k} L’implication est valideà condition d’ajouter àψ1 la propriétéj∈Nqui avec le testj < Npermet
de démontrerj+ 1≤N ψ 5
(1 pt)À partir de la propriétéψs , on détermine la propriétéψ5 grâce à la transitionq5 result:=false
−−−−−−−−−→
affectationq s. Cette transition fait uniquement des affectations donc le meilleur choix pourψ5 est :ψ 5def =ψs [ � result← false]≡ { �
result=true=⇒( ∀k∈[0..N−1], G[F[k]] =k) � result=false=⇒( ∃k∈[0..N−1], G[F[k]]6=k) }[ � result← � true] ≡{ false=true=⇒( ∀k∈[0..N−1], G[F[k]] =k) false=false=⇒( ∃k∈[0..N−1], G[F[k]]6=k) ≡ ∃k∈[0..N−1], G[F[k]]6=k �
vérification 2(1 pt)Les propriétésψ3 etψ5 étant choisies, on utilise la transitionq3 G[F[j]]6=j
−−−−−−−→test q5 pour vérifier que
les propriétés que nous avons choisies sont bien des invariants. Cette transition effectue un test, elle doit
donc satisfaire l’implication suivante :ψ 3
∧G[F[j]]6=j︸︷︷︸ test? =⇒ψ5 On choisit d’ajouter àψ3 la propriété0≤j; l’implication est alors valide.
Preuve de validité de l’implication:On peut démontrerψ5 :∃k∈[0..N−1], G[F[k]]6=ken
choisissantk=jpuisque
—0≤jetj+ 1≤Nd’aprèsψ3 , ce qui donne0≤j≤N−1c’est-à-direj∈[0..N−1]
—G[F[j]]6=jd’après le test.
M.PérinUniversité Grenoble-Alpes3
Automate & Grammairespolytech’ grenoble/ricm3 �
conclusion(1 pt)Les vérifications nous ont amené à modifier les propriétésψ1 etψ3 comme suit :ψ 1def = j∈N j≤N ∀k∈[ � 0.. j−1 ], G[F[k]] =k etψ3 def= 0≤j j+ 1≤N∀k∈[ � 0..
j−1 ], G[F[k]] =k avec ces modifications toutes les implications sont valides.
Conclusion :les propriétésψ1 ,ψ2 ,ψ3 ,ψ4 ,ψ5 ,ψs sont 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 j:=0−−−→ affectationq 1
. Cette transition fait
uniquement des affectations donc le meilleur choix pourψ0 est :ψ 0def =ψ1 [j←0]≡ j∈N j≤N
∀k∈[0..j−1], G[F[k]] =k [j←0]≡ 0∈N0≤N ∀k∈[0..−1]︸ ︷︷︸∅ , G[F[k]] =k≡0≤N Conclusion :le programme est correct si on l’utilise pour un tableau ayant un nombre de caseN≥0.
Exercice 2(9 pt)Preuve de correction partielle de l’algorithme d’ex-
ponentiation rapide
Algorithme
x:=A ; y:=N ; r:=1 ;
while(y>0){
if (y%2=0){ x:=x*x; y:=y/2; }
else { r:=r*x; y:=y-1; }} Q1.(1 pt)Donnez les transitions de l’automate pour qu’il corresponde au programme précédent.// q0 x←A;y←N;r←1 qs q1 y≤011 y>0 q3 x:=x×x;y:=y/211 q4 r:=r×x;y:=y−1mm q2 ymod26=0CC ymod2=0[[ M.PérinUniversité Grenoble-Alpes4
Automate & Grammairespolytech’ grenoble/ricm3
Q2.(1 pt)Complétez l’exécution de l’automate en adoptant la présentation ci-dessous.
a) Pour les valeursA= 3, N= 3étatq 0q 1q 2q 4q 1q 2q 3q 1q 2q 4q 1q s
x?33339999999
y?33221111000
r?11333333272727
b) Même question pour les valeursA= 2, N= 0
solutionétatq 0q 1q sx?22 y?00r?11 Q3.(0.5 pt)Donnez la propriété de correction qui exprime qu’à la sortie de l’automate la variable
rcontient la valeur deAN .
solutionψ sdef =r=AN ∧y= 0
Q4.(6 pt)Preuve de correction partielle (soignez la rédaction !)Donnez et démontrez
l’implication associée à chaque transition et donnez les 5 invariants(ψs ,ψ1 ,ψ3 ,ψ4 ,ψ2 )associés auxétatsq s,q 1,q 3,q 4,q 2. Indication :ψ1 def=r×x y=A N∧y≥0 solution
— La transitionq1 y≤0−−−→q s
nous impose de choisirψ1 de sorte qu’on ait l’implicationψ 1
∧y≤0 =⇒ψ s︷ ︸︸︷r=A N
∧y= 0
On choisitψ 1def =r×xy =AN ∧y≥0
— La transitionq4 r:=r×x;y:=y−1
−−−−−−−−−−−−→q1 comporte uniquement des instructions d’affectations donc le meilleur
choix pourψ4 est :ψ 4def =ψ1 [r←r×x;y←y−1]def = (r×x)×x(y−1) =AN ∧y−1≥0≡r×xy =AN ∧y≥1
— La transitionq3 x:=x×x;y:=y/2
−−−−−−−−−−−−→q1 comporte uniquement des instructions d’affectations donc le meilleur
choix pourψ3 est :ψ 3def =ψ1 [x←x×x;y←y/2]def =r×(x2 )(y/2) =AN ∧y/2≥0≡r×x2(y/2) =AN ∧y≥0
— La transitionq2 ymod2=0
−−−−−−−→q3 nous impose de choisirψ2 de sorte qu’on ait l’implicationψ 2
∧ymod2 = 0? =⇒ψ 3︷ ︸︸︷r×x 2(y/2)=A N∧y≥0 Preuve de l’implication:D’après le testymod2 = 0, on a donc l’égalité2(y/2) =yet on peut
simplifierψ3 enr×xy =AN ∧y≥0. On choisit alorsψ 2def =r×xy =AN ∧y≥0
M.PérinUniversité Grenoble-Alpes5
Automate & Grammairespolytech’ grenoble/ricm3
et l’implication devient triviale puisqu’elle est de la formeP⇒P
— Étape de
VÉRIFICATION:ψ1 ,ψ2 etψ4 sont connues donc on peut utiliser les transitionsq1 y>0−−−→q 2etq 2
ymod26=0
−−−−−−−→q4 pourvérifier nos choix. Nos choix sont valides s’ils permettent de montrer les implica-
tions :ψ 1︷ ︸︸︷r×x y=A N
∧y≥0∧y >0ok =⇒ψ 2︷︸︸︷ r×xy =AN ∧y≥0et ψ2 ︷︸︸︷r×x y=A N
∧y≥0∧ymod26= 0ok =⇒ψ 4︷ ︸︸︷r×x y=A N∧y≥1 car 1 est le plus petit nombre entier≥0.
Q5.(0.5 pt)En déduire les conditions d’utilisations du programme.
solutionψ 0def =ψ1 [x←A;y←N;r←1]def = (r×xy =AN ∧y≥0)[x←A;y←N;r←1]def = 1×AN =AN ∧N≥0def =N≥0
Le résultatr=AN à la sortie du programme est guarantie pourN≥0
M.PérinUniversité Grenoble-Alpes6