“doc” (Col. : Science Sup 17x24) — 2007/7/19 — 18:18 — page 130 — #140
i
i
i
i
i
i
i
i
130
3
• Techniques de programmation déclarative
Dans l’appel {IterLength I Ys}, il y a un deuxième argument avec valeur
initiale de 0. Nous pouvons cacher cet argument en définissant IterLength comme
une procédure locale. La définition finale de Length est donc
local
fun {IterLength I Ys}
case Ys of nil then I
[] _|Yr then {IterLength I+1 Yr} end
end
in
fun {Length Xs} {IterLength 0 Xs} end
end
ce qui définit un calcul itératif pour calculer la longueur d’une liste. Nous définissons
IterLength à l’extérieur de Length. Cela nous permet d’éviter de créer une
nouvelle valeur procédurale à chaque appel de Length. Il n’y a pas d’avantage à
définir IterLength à l’intérieur de Length, parce qu’elle n’utilise pas l’argument
Xs de Length.
Nous pouvons utiliser la même technique pour Reverse que celle que nous avons
utilisée pour Length. Dans le cas de Reverse, l’état contient l’inverse de la partie
de la liste déjà vue au lieu de sa longueur. La mise à jour de l’état est facile : il suffit
d’ajouter un nouvel élément au début de la liste. L’état initial est nil. Ces idées nous
donnent la version suivante de Reverse :
local
fun {IterReverse Rs Ys}
case Ys of nil then Rs
[] Y|Yr then {IterReverse Y|Rs Yr} end
end
in
fun {Reverse Xs} {IterReverse nil Xs} end
end
Cette version de Reverse a un temps linéaire et une exécution itérative.
e) L’exactitude avec les invariants d’état
Prouvons que IterLength est correct. Nous utiliserons une technique générale qui
fonctionne bien pour IterReverse et d’autres calculs itératifs. L’idée est de définir
une propriété P(S i ) de l’état et de prouver qu’elle est toujours vraie. On dit que P(S i )
est un invariant d’état. Si P est bien choisi, l’exactitude du calcul sera une conséquence
de P(S final ). Pour IterLength nous définissons P comme ceci :
P((i, Ys)) ≡ (length(Xs) = i + length(Ys))