On considère l’algorithme suivant :

Input : x1 ∈ ℕ, x2 ∈ ℕ*
Output : (z1, z2)

y1 ← 0
y2 ← x1
while y2 ≥ x2 do
  y1 ← y1 + 1
  y2 ← y2 − x2
return (z1 = y1, z2 = y2)

1. Donner précisément la précondition $\phi(e)$.
2. Donner la postcondition $\psi(e,s)$.
3. Identifier un variant de boucle et justifier qu’il permet de conclure à la terminaison.
4. Proposer un invariant de boucle.
5. Montrer que l’invariant est vrai :
6. avant l’entrée dans la boucle ;
7. après une itération quelconque.
8. Conclure sur la correction totale de l’algorithme.

On considère l’algorithme suivant :

Input : N ∈ ℕ*
Output : S ∈ {Vrai, Faux}

m ← N
pair ← Vrai
while m > 1 et pair do
  pair ← (m est pair)
  m ← ⌊m / 2⌋
return pair

1. Expliquer pourquoi la condition $N \neq 0$ est nécessaire.
2. Donner la postcondition $\psi(e, s)$ sous-forme logique.
3. Montrer que la boucle se termine.
4. On note $k$ le nombre d'itérations déjà effectuées.
5. Proposer une relation reliant $N$, $m$ et $k$.
6. Montrer que cette relation est un invariant.
7. Conclure que l'algorithme est correct.

Indication : raisonner séparément selon que pair est vrai ou faux à la sortie de la boucle.

Soit un tableau T contenant $N \geq 1$ éléments d’un ensemble totalement ordonné.

m ← T[1]
for i = 2 to N do
  if T[i] > m then
    m ← T[i]
return m

1. Donner la précondition et la postcondition.
2. La terminaison est-elle immédiate ? Justifier.
3. Formuler un invariant de boucle en langage mathématique.
4. Montrer que cet invariant est conservé à chaque itération.
5. En déduire la correction de l’algorithme.

On considère l’algorithme suivant :

Input : x1, x2 ∈ ℕ*
Output : z

a ← x1
b ← x2
if a < b then échanger(a,b)
while b > 0 do
  (q, r) ← divEuclide(a, b)
  a ← b
  b ← r
end while
return z = a

1. Donner les prédicats $\phi(e)$ et $\psi(e,s)$.
2. Proposer un variant de boucle et justifier la terminaison.
3. Proposer un invariant de boucle fondé sur le pgcd.
4. Justifier rigoureusement l’invariance à l’aide des propriétés du pgcd.
5. Conclure sur la correction totale de l’algorithme.

On considère l’algorithme suivant, dont on ne précise pas la fonction attendue.

Entrée : x ∈ ℕ*
Sortie : z ∈ ℕ
a ← x
b ← 0
while a > 0 do
    if a est impair then
        b ← b + 1
    end if
    a ← ⌊a / 2⌋
end while
return z = b

1. Compréhension de l’algorithme
2. Exécuter l’algorithme pour les valeurs suivantes de x :
3. x = 1
4. x = 5
5. x = 13
6. Présenter les valeurs successives de a et b.
7. À partir de ces exemples, conjecturer le rôle de l’algorithme : que calcule-t-il exactement ?
8. Spécification
9. Donner la précondition $\phi(e)$.
10. Donner la postcondition $\psi(e,s)$.
11. Terminaison
12. Identifier le variant de boucle.
13. Justifier que ce variant : est à valeur entière, est borné, est strictement décroissant à chaque itération.
14. Conclure que l'algorithme se termine pour toute entrée vérifiant $\psi(e)$.
15. Correction - On note $a_k$ et $b_k$ les valeurs des variables $a$ et $b$ après $k$ itérations de la boucle, et $x$ la valeur d'entrée initiale.
16. Proposer un invariant de boucle relient $x$, $a$ et $b$ et $k$ le nombre d'itérations.
17. Montrer que cet invariant est valide tout le long de l'algorithme.
18. En utilisant la condition d'arrêt de boucle, montrer que $\psi(e, s)$ est vérifiée à la fin de l'algorithme.
19. Conclure que cet algorithme est totalement correct.