Variante de boucle - Loop variant

En informatique , une variante de boucle est une fonction mathématique définie sur l' espace d'état d'un programme informatique dont la valeur est diminuée de façon monotone par rapport à une relation (stricte) bien fondée par l'itération d'une boucle while sous certaines conditions invariantes , assurant ainsi sa résiliation . Une variante de boucle dont la plage est limitée aux entiers non négatifs est également appelée fonction liée , car dans ce cas, elle fournit une limite supérieure triviale sur le nombre d'itérations d'une boucle avant qu'elle ne se termine. Cependant, une variante de boucle peut être transfinie et n'est donc pas nécessairement limitée aux valeurs entières.

Une relation bien fondée est caractérisée par l'existence d'un élément minimal de chaque sous-ensemble non vide de son domaine. L'existence d'une variante prouve la terminaison d'une boucle while dans un programme informatique par descendance bien fondée . Une propriété de base d'une relation bien fondée est qu'elle n'a pas de chaînes descendantes infinies . Par conséquent, une boucle possédant une variante se terminera après un nombre fini d'itérations, tant que son corps se terminera à chaque fois.

Une boucle while , ou, plus généralement, un programme informatique pouvant contenir des boucles while, est dite totalement correcte si elle est partiellement correcte et qu'elle se termine.

Règle d'inférence pour une exactitude totale

Afin d'énoncer formellement la règle d'inférence pour la fin d'une boucle while que nous avons démontrée ci-dessus, rappelons que dans la logique Floyd-Hoare , la règle pour exprimer l'exactitude partielle d'une boucle while est :

${\displaystyle {\frac {\{I\land C\}\;S\;\{I\}}{\{I\}\;{\mathtt {while}}\;C\;{\mathtt { faire}}\;S\;\{I\land \lnot C\}}},}$

où I est l' invariant , C est la condition et S est le corps de la boucle. Pour exprimer l'exactitude totale, nous écrivons à la place :

${\displaystyle {\frac {<{\text{ est bien fondé}},\;[I\land C\land V=z]\;S\;[I\land V<z]}{[I] \;{\mathtt {while}}\;C\;{\mathtt {do}}\;S\;[I\land \lnot C]}},}$

où, de plus, V est la variante , et par convention le symbole non lié z est considéré comme universellement quantifié .

Chaque boucle qui se termine a une variante

L'existence d'une variante implique qu'une boucle while se termine. Cela peut paraître surprenant, mais l'inverse est vrai aussi, tant que l'on suppose l' axiome du choix : chaque boucle while qui se termine (étant donné son invariant) a une variante. Pour le prouver, supposons que la boucle

${\displaystyle {\mathtt {while}}\;C\;{\mathtt {do}}\;S}$

se termine étant donné l'invariant I où nous avons l'assertion de correction totale

${\displaystyle [I\land C]\;S\;[I].}$

Pensez à la relation « successeur » sur l'espace d' état Σ induit par l'exécution de l'instruction S à partir d' un état satisfaisant à la fois l'invariant I et l'état C . C'est-à-dire que nous disons qu'un état σ′ est un "successeur" de σ si et seulement si

• Je et C sont vraies dans l'état σ , et
• σ′ est l'état qui résulte de l'exécution de l'instruction S dans l'état σ .

Nous notons que sinon la boucle ne se terminerait pas. ${\displaystyle \sigma '\neq \sigma ,}$

Considérons ensuite la clôture réflexive et transitive de la relation de « successeur ». Appelons cette itération : on dit qu'un état σ′ est un itéré de σ si l'un ou l' autre ou s'il existe une chaîne finie telle que et est un "successeur" de pour tout I ,${\displaystyle \sigma '=\sigma ,}$${\displaystyle \sigma _{0},\sigma _{1},\,\dots \,,\sigma _{n}}$${\displaystyle \sigma _{0}=\sigma ,}$ ${\displaystyle \sigma _{n}=\sigma '}$${\displaystyle \sigma _{i+1}}$${\displaystyle \sigma _{i};}$${\style d'affichage 0\leq i<n.}$

Nous notons que si σ et σ ' sont deux états distincts, et σ' est un itérateur de σ , alors σ ne peut pas être un itérateur de σ ', pour encore une fois, sinon la boucle ne permettrait pas de mettre fin. En d'autres termes, l'itération est antisymétrique, et donc, un ordre partiel .

Maintenant, puisque la boucle while se termine après un nombre fini d'étapes étant donné l'invariant I , et qu'aucun état n'a de successeur à moins que I ne soit vrai dans cet état, nous concluons que chaque état n'a qu'un nombre fini d'itérations, chaque chaîne descendante par rapport à l'itération n'a qu'un nombre fini de valeurs distinctes, et donc il n'y a pas de chaîne descendante infinie , c'est-à-dire que l'itération de boucle satisfait la condition de chaîne descendante .

Par conséquent, en supposant l' axiome du choix , la relation « successeur » que nous avons définie à l'origine pour la boucle est bien fondée sur l'espace d'état Σ , car elle est stricte (irréflexive) et contenue dans la relation « itérer ». Ainsi, la fonction d'identité sur cet espace d'état est une variante de la boucle while, car nous avons montré que l'état doit strictement décroître - en tant que "successeur" et "itérer" - chaque fois que le corps S est exécuté étant donné l'invariant I et la condition C .

De plus, nous pouvons montrer par un argument de comptage que l'existence d'une variante implique l'existence d'une variante dans ω ₁ , le premier ordinal indénombrable , à savoir,

${\displaystyle V:\Sigma \rightarrow \omega _{1}.}$

En effet , la collection de tous les états accessibles par un programme informatique fini dans un nombre fini d'étapes d'une entrée est finie dénombrable et ω ₁ est l'énumération de tous les bien-commande types sur des ensembles dénombrables.

Considérations pratiques

En pratique, les variantes de boucle sont souvent considérées comme des entiers non négatifs , ou même tenus de l'être, mais l'exigence que chaque boucle ait une variante entière supprime le pouvoir expressif de l' itération illimitée d'un langage de programmation. À moins qu'un tel langage (formellement vérifié) permette une preuve transfinie de terminaison pour une autre construction tout aussi puissante telle qu'un appel de fonction récursif , il n'est plus capable de -récursivité complète , mais seulement de récursivité primitive . La fonction d'Ackermann est l'exemple canonique d'une fonction récursive qui ne peut pas être calculée dans une boucle avec une variante entière .

En termes de complexité de calcul , cependant, les fonctions qui ne sont pas récursives primitives se situent bien au-delà du domaine de ce qui est généralement considéré comme traitable . Considérant même le cas simple de l'exponentiation en tant que fonction récursive primitive, et que la composition des fonctions récursives primitives est récursive primitive, on peut commencer à voir à quelle vitesse une fonction récursive primitive peut croître. Et toute fonction qui peut être calculée par une machine de Turing dans un temps d'exécution borné par une fonction récursive primitive est elle-même récursive primitive. Il est donc difficile d'imaginer une utilisation pratique de la μ -récursion complète où la récursivité primitive ne fera pas l'affaire, d'autant plus que la première peut être simulée par la seconde jusqu'à des temps d'exécution excessivement longs.

Et dans tous les cas, le premier théorème d'incomplétude de Kurt Gödel et le problème de l' arrêt impliquent qu'il existe des boucles while qui se terminent toujours mais ne peuvent pas être prouvées ; il est donc inévitable que toute exigence d'une preuve formelle de terminaison doive réduire le pouvoir expressif d'un langage de programmation. Bien que nous ayons montré que chaque boucle qui se termine a une variante, cela ne signifie pas que le bien-fondé de l'itération de la boucle peut être prouvé.

Exemple

Voici un exemple, en pseudocode de type C , d'une variante entière calculée à partir d'une limite supérieure du nombre d'itérations restantes dans une boucle while. Cependant, C permet des effets secondaires dans l'évaluation des expressions, ce qui est inacceptable du point de vue de la vérification formelle d'un programme informatique.

/** condition-variable, which is changed in procedure S() **/
bool C;
/** function, which computes a loop iteration bound without side effects **/
inline unsigned int getBound();

/** body of loop must not alter V **/ 
inline void S(); 

int main() {
    unsigned int V = getBound(); /* set variant equal to bound */
    assert(I); /* loop invariant */
    while (C) {
        assert(V > 0); /* this assertion is the variant's raison d'être (reason of existence) */
        S(); /* call the body */
        V = min(getBound(), V - 1); /* variant must decrease by at least one */
    };
    assert(I && !C); /* invariant is still true and condition is false */

    return 0;
};

Pourquoi même envisager une variante non entière ?

Pourquoi même envisager une variante non entière ou transfinie ? Cette question a été soulevée parce que dans tous les cas pratiques où nous voulons prouver qu'un programme se termine, nous voulons également prouver qu'il se termine dans un laps de temps raisonnable. Il y a au moins deux possibilités :

• Une limite supérieure du nombre d'itérations d'une boucle peut être conditionnelle à la preuve de la terminaison en premier lieu. Il peut être souhaitable de prouver séparément (ou progressivement) les trois propriétés de
  • exactitude partielle,
  • résiliation, et
  • temps de course.
• Généralité : considérer des variantes transfinies permet de voir toutes les preuves possibles de terminaison pour une boucle while en termes d'existence d'une variante.

Voir également

• Alors que la boucle
• Invariant de boucle
• Induction transfinie
• Condition de la chaîne descendante
• Grand ordinal dénombrable
• Rectitude (informatique)
• Conditions préalables les plus faibles de la boucle While

Les références