TD1 : Correction/Spécification/Terminaison

Énoncé

Algorithmique : Rappels

  • Spécification
  • Correction
    • Correction partielle
    • Terminaison
  • Complexité

Spécification (Hoare)

∃ pré-conditions et post-conditions que doivent vérifier l’algorithmique

Ex:

factorielle n =
∣ 1 si n = 0
∣ n*factorielle(n-1) sinon

Préconditions : $in = v ∧ in \geq 0$

Fact(in, out)

Postconditions : $out = v!$

Correction

$in = v ∧ in \geq 0$

Fact(in, out):
out ← 1

while in > 0 do
  out ← out * in
  in ← in-1
end
return

$out = v!$

Procédure : trouver un invariant de boucle qui “tient” à chaque itération de la boucle

Invariant de boucle : $out * in! = v!$

Terminaison

Ensemble bien fondé ≝ $(E, <)$ où \(\not \exists (v_i)_{i ∈ ℕ}; \, \, \, v_{i+1} < v_i\)

Th : Le produit cartésien d’ensemble bien fondés (muni de l’ordre lexicographique) est bien fondé

Preuve par l’absurde. Si $\exists (e, f)$ tq $\forall i, (e_i, f_i)$ : alors $e$ OU $f$ est ultimement strictement décroissante.

Complexité

Définitions de $o, O, 𝛳, 𝛺$

Exercices

EX1

function PGCD(x: integer, y: integer){
if x == 0 { return y }
if x >= y then
  return PGCD(y,x)
else
  return PGCD(x, y-x)
}

1.

Spécification :

Préconditions : $x, y = v, w ∧ x,y \geq 0$

PGCD(in, out)

Postconditions : $out = PGCD(v,w)$

2.

  function PGCD(x: integer, y: integer){
  if x > y then
    return PGCD(y,x)
  else
    return PGCD(x, y-x)
  }
  • Terminaison : la suite des x décroît ultimement strictement (et est strictement positive)
  • Correction : Si $x \leq y, PGCD(x,y) = PGCD(x,y-x)$ car \(div(x) ∩ div(y) = div(x) ∩ div(y-x)\) où $div$ = ensemble des diviseurs

EX2

function find(t: sorted integer array, x: integer, low: integer, high: entier){
while low < high do {
  tmp <- (low+high) / 2
  if t[tmp] < x then
    low <- tmp
  else
    high <- tmp
done
return low
}
}

1.

Spécification :

Préconditions : $t$ tableau trié, $x ∈ t, low, high$ entiers positifs, où $high \leq len(t)$

find(t, x, low, high)

Postconditions : $low$ est l’indice de $x$ si $x ∈ t$, $-1$ sinon

2.

function find(t: sorted integer array, x: integer, low: integer, high: entier)
{
  while low < high-1 do
  {
    tmp <- (low+high) / 2
    if t[tmp] < x then
      low <- tmp
    else
      high <- tmp
  }
  done
  if t[low] = x { return low}
  else return high
}

  • Terminaison : la suite (high-low) décroît strictement (et est strictement positive) (variant: high-low)

  • Correction : Invariant de boucle : \(t[low] \leq x \leq t[high] ∧ (high-low \geq 0)\)

EX3

1.

minmax(T){
  mini, maxi <- T[0], T[0]
  n <- len(T)-1
  for(j=1; j<n; j++)
  {
    if T[j] < mini { mini <- T[j]}
    if T[j] > maxi { maxi <- T[j]}
  }
  return mini, maxi
}
  • Correction :

Invariant de boucle : \(mini \leq T[0], …, T[j-1] ∧ maxi \geq T[0], …, T[j-1]\) et il existe des indices en lesquels $min(T), max(T)$ sont atteints.

Dans le pire cas : $2(len(T)-1)$ comparaisons sont effectuées.

2.

minmax(T){
  mini, maxi <- T[0], T[0]
  n <- len(T)-1
  for(j=1; j<(n+1)/2; j++)
  {
    if T[j] < T[n-j] { mi <- T[j]; ma <- T[n-j] }
    if mi < mini { mini <- mi }
    if ma > maxi { maxi <- ma }
  }
  return mini, maxi
}

Dans le pire cas : $3 ⸤len(T)/2⸥ $ comparaisons sont effectuées.

EX4

1.

fibo(n){
  if n = O or n=1 { return n }
  else { return fibo(n-1) + fibo(n-2)}
}

  • Terminaison : la suite des arguments décroît strictement dans $ℕ$

  • Correction : par une récurrence immédiate

  • Complexité : \(T(n) = \begin{cases} 1 + T(n-1) + T(n-2) \text{ si } n \geq 2 \\ 0 \text{ sinon }\end{cases}\)

Donc \(T(n) = 𝛳(𝜑^n)\)

MIEUX : récursivité terminale :

fibo(n){
  if n = O or n=1 { return n }
  aux(i,a,b) {
      if i = 1 { return b }
      else {
        aux(i-1,b,a+b)
      }
  }
  aux(n, 0, 1)
}

fibo(n){
  if n = O or n=1 { return n }
  else {
    a, b = 0, 1
    for(i=2; i<=n; i++){
      a, b = b, a+b
    }
    return b
}
}

  • Terminaison : immédiate.

  • Correction : Invariant de boucle : \(a = f_{i-2}, b = f_{i-1}\)

  • Complexité : linéaire.

2.

PGCD(a,b){
  if a = 0 { return b }
  if b = 0 { return a }
  else {
    return PGCD(b,a%b)
  }
}

  • Terminaison : le deuxième argument décroît strictement ultimement dans $ℕ$.

  • Correction : \(PGCD(a,b) = PGCD(b, a\%b)\)

PGCD(a,b){
  if a = 0 { return b }
  if b = 0 { return a }
  else {
    r <- a%b
    while r > 0 do {
    a, b = b, r
    }
  return b
  }
}

  • Terminaison : $r$ décroît strictement ultimement dans $ℕ$.

  • Correction : \(PGCD(a,b) = PGCD(b, a\%b)\)

  • Complexité : Toutes les 2 étapes, on divise au moins par $2$ \(T(n) = O(log_2(max(a,b)))\)

x, y :int

pgcd(x,y) = pgcd(y, x%y) = pgcd(x%y, y%(x%y))

  • Cas 1 : $y > x/2 ⟹ x = y + x\%y$ ⟶ $x\%y \leq x/2$

  • Cas 2 : $y \leq x/2 ⟹ x\%y < y \leq x/2$

Toutes les 2 étapes : division par 2 au moins.

Leave a comment