Boucles, tableaux et invariants

Un résultat se construit étape par étape

Une boucle n’est pas seulement une répétition. C’est un calcul découpé en états successifs. Pour la comprendre, nommez les valeurs qui changent, notez leur valeur initiale, puis décrivez exactement ce que fait un passage.

Voici un patron d’addition sur un tableau de trois entiers :

proc somme(valeurs: [3]i64) -> i64 {
    let mut index: i64 = 0;
    let mut total: i64 = 0;

    while index < 3 {
        set total = total + valeurs[index];
        set index = index + 1;
    }

    return total;
}

À chaque passage, index désigne l’élément à ajouter ; après l’ajout, il avance d’une position. Le tableau fournit les indices 0, 1 et 2 : la condition index < 3 empêche la lecture à l’indice 3. Les tableaux fixes, l’indexation, while et set sont couverts par des exemples du dépôt. Ce programme combiné est un patron pédagogique, pas une fixture testée telle quelle.

Écrire l’invariant avant le corps

Un invariant est une phrase qui reste vraie au début de chaque passage. Pour la somme précédente, on peut écrire :

total contient la somme des éléments déjà parcourus, de l’indice 0 jusqu’à index - 1.

Vérifiez cette phrase en trois temps :

1. Initialisation. Avant le premier passage, index vaut 0 et aucune valeur n’a été parcourue. La somme vide vaut 0 ; total est donc correct.
2. Conservation. Si l’invariant est vrai et que index < 3, le corps ajoute exactement valeurs[index], puis avance index de 1. total correspond alors à tous les éléments parcourus.
3. Sortie. La boucle s’arrête quand index vaut 3. Les trois éléments ont été parcourus ; l’invariant donne le résultat attendu.

Cette méthode trouve les erreurs de borne avant l’exécution. Si vous commencez à 1, le premier élément manque. Si vous écrivez index <= 3, le programme tente de lire un quatrième élément.

Mesurer la progression

Un invariant ne suffit pas : une boucle doit aussi s’arrêter. Ici, index augmente de 1 et reste inférieur à 3 tant que le corps recommence. La distance 3 - index diminue ; elle ne peut pas diminuer indéfiniment tout en restant positive. Pour une boucle plus complexe, cherchez une quantité entière qui se rapproche visiblement de zéro.

Avec continue, vérifiez que le chemin qui saute le reste du corps fait tout de même progresser l’état. Avec break, précisez les valeurs possibles à la sortie anticipée. Une boucle qui se termine à plusieurs endroits a plusieurs postconditions à examiner.

Tracer une boucle réelle du dépôt

Dans controle.vit, l’indice avance jusqu’à 6. L’itération 3 est ignorée avec continue ; l’itération 6 arrête la boucle avec break avant d’être ajoutée. Les valeurs ajoutées sont donc 1, 2, 4 et 5, pour un total de 12. L’exemple se lance avec :

build/bin/vitte run examples/tutorials/controle.vit --quiet --no-color

Résultat confirmé dans le dépôt : code de sortie 0. Une trace sous forme de tableau rend chaque transition explicite avec les colonnes indice, branche choisie et total. L’exemple tableaux.vit vérifie également la lecture et l’écriture d’éléments indexés.

Un algorithme, trois preuves

Avant d’ajouter un parcours dans un programme, préparez trois réponses : pourquoi le premier indice est valide, pourquoi chaque passage garde l’indice valide, et pourquoi le dernier passage s’arrête avant la borne interdite. Cette courte preuve fait partie de la conception du programme ; elle ne dépend pas d’un message du compilateur.

Exemple détaillé : rechercher une valeur

La recherche séquentielle visite les indices dans l’ordre jusqu’à trouver la cible ou atteindre la longueur. Voici une version pédagogique pour trois éléments :

proc contient(valeurs: [3]i64, cible: i64) -> bool {
    let mut index: i64 = 0;
    while index < 3 {
        if valeurs[index] == cible {
            return true;
        }
        set index = index + 1;
    }
    return false;
}

Avant chaque passage, l’invariant est : « aucun indice plus petit que index ne contient la cible ». Si la comparaison réussit, la procédure peut renvoyer vrai immédiatement. Sinon, augmenter l’indice étend la zone déjà examinée d’un élément. À la sortie, l’indice vaut 3 et tous les éléments ont été examinés : l’invariant permet de renvoyer faux.

Cette combinaison complète est un exemple d’étude, pas une fixture du dépôt confirmée telle quelle. Les boucles, les tableaux et les comparaisons sont présents dans des exemples exécutés ; vérifiez leur combinaison exacte avant de l’utiliser comme preuve de compilation.

Éviter les bornes cachées

Dans les exemples fixes, la longueur apparaît comme un nombre tel que 3. Si vous répétez ce nombre dans plusieurs conditions, déclarations et tailles, une modification peut laisser une borne oubliée. Une constante nommée peut rendre le lien visible lorsque la prise en charge de cette constante est confirmée. Avec une taille connue au type, écrivez au minimum un commentaire ou un contrat expliquant pourquoi la borne de la boucle correspond au nombre d’éléments.

Les plages 0..3 sont demi-ouvertes dans les conventions documentées : elles incluent 0, 1 et 2. Mais l’opérateur de plage et for ne sont pas confirmés au runtime dans tous les cas. Dans cette démonstration, le test explicite index < 3 rend les accès plus faciles à vérifier.

Étendre une trace à un cas vide

Un tableau fixe de longueur zéro n’est pas utilisé dans les fixtures de cette leçon, mais le raisonnement de boucle reste instructif : si la longueur vaut zéro, la condition de parcours est fausse avant le premier accès et la somme initialisée à zéro est renvoyée. Cette propriété s’appelle souvent le cas vide. Pour des collections réelles, vérifiez que le type et le backend acceptent cette taille avant de compter dessus.

Pour une recherche, le même cas vide doit renvoyer faux sans lire de mémoire. Un invariant bien formulé vous permet de vérifier ce comportement sans inventer un indice spécial.

Un invariant relie le passé de la boucle à son état courant

Pour la somme d’un tableau, l’invariant total = somme des valeurs d’indices compris entre 0 et index - 1 relie les données déjà parcourues au couple d’état (index, total). Il est vrai avant la boucle parce que l’intervalle parcouru est vide et que le total initial vaut zéro. Pendant un passage, la valeur d’indice index est ajoutée, puis l’indice augmente : l’intervalle décrit par l’invariant s’étend exactement d’une position.

À la sortie, index == 3. La même phrase indique alors que le total contient les éléments 0, 1 et 2, donc tous les éléments du tableau. La preuve repose sur la signification de l’état et de la condition, pas sur l’apparence du code. Si l’ordre des mises à jour change, il faut réexaminer l’invariant : une formule correcte pour une boucle peut devenir fausse après un déplacement de ligne.

La progression garantit la terminaison

La correction d’une boucle comporte deux propriétés. L’invariant montre que les résultats intermédiaires ont le sens voulu ; une mesure de progression montre que la répétition peut s’arrêter. Ici, 3 - index est un entier non négatif tant que la boucle continue et diminue à chaque passage. Si le corps ne change pas index, cette mesure reste constante et rien n’explique la sortie.

Les sorties anticipées modifient le raisonnement. Un break peut terminer la boucle avant que index atteigne 3 ; l’état final doit alors être décrit par la condition de cette sortie. Un continue peut sauter une mise à jour et empêcher la progression. Pour un contrôle vérifié du dépôt, l’exemple additionne 1, 2, 4 et 5 ; l’indice 3 est ignoré, puis l’indice 6 arrête la boucle avant l’addition.

La recherche séquentielle : deux postconditions

La recherche d’une cible dans un tableau fixe possède deux sorties sémantiquement différentes. Si la comparaison réussit à l’indice index, la procédure renvoie vrai et l’existence de la cible est établie. Si l’indice atteint la longueur sans correspondance, tous les éléments ont été examinés et faux est justifié. L’invariant « aucun indice inférieur à index ne contient la cible » explique pourquoi la seconde sortie est correcte.

Le cas vide est naturellement couvert par le même raisonnement : l’indice commence à zéro et la condition index < longueur est immédiatement fausse pour une longueur nulle. Aucun accès mémoire n’a lieu et la recherche renvoie faux. Cette propriété conceptuelle ne prouve pas que chaque backend accepte un tableau de longueur zéro ; elle démontre que la forme de l’algorithme ne demande aucun indice quand la collection est vide.

Invariant et postcondition d’une recherche

Pour la recherche de 7 dans [4, 7, 2], l’indice 0 vérifie que la première valeur est différente de la cible ; l’invariant affirme alors que le préfixe de longueur 1 ne contient pas la cible. À l’indice 1, la comparaison réussit et la procédure retourne vrai. Pour la cible 9, l’invariant s’étend successivement aux préfixes de longueur 1, 2 et 3 ; la sortie normale permet de conclure que la cible est absente.

La même structure de boucle prend en charge une sortie anticipée et une sortie par épuisement. La première prouve la présence ; la seconde prouve l’absence parce que chaque position valide a été visitée. L’invariant relie ce qui a été examiné à la conclusion retournée. Sans cette relation, un simple return false à la fin ne dit pas pourquoi aucune position oubliée ne pourrait contenir la cible.

Invariants pour d’autres accumulateurs

Un accumulateur ne contient pas nécessairement une somme. Il peut conserver le plus grand élément rencontré, le nombre de valeurs conformes ou un indicateur de présence. Chaque forme demande un invariant différent : le maximum courant doit être le maximum du préfixe ; un compteur doit égaler le nombre de cas conformes déjà observés ; un indicateur doit refléter si la cible est apparue dans la partie parcourue.

Le choix de la valeur initiale dépend de ce sens. La somme vide vaut zéro, mais un maximum n’a pas toujours une valeur initiale naturelle dans le domaine. Il faut alors utiliser le premier élément, une représentation nullable, ou un état pick explicite si ces formes sont supportées. L’initialisation est une partie de la preuve, pas une ligne arbitraire avant la boucle.