Étude du calculateur de panier

Comportement du calculateur

Notre panier contient des lignes. Chaque ligne a un prix unitaire et une quantité. Le total correspond à la somme des sous-totaux. Le calculateur étudié produit un total et refuse les valeurs incohérentes. Cette version reste volontairement petite : aucun fichier, réseau ou affichage n’est nécessaire pour comprendre la logique.

Modèle de données : une ligne de panier

Une ligne possède deux données à la fois. Une form est donc plus claire que deux nombres isolés transmis à toutes les procédures :

space cours::panier;

form Ligne {
    prix_unitaire: i64,
    quantite: i64,
}

proc sous_total(ligne: &Ligne) -> i64 {
    return ligne.prix_unitaire * ligne.quantite;
}

Le nom Ligne représente une idée du domaine. La procédure sous_total reçoit une référence car elle a besoin de lire les champs sans transformer la ligne. La multiplication est au même endroit pour tous les appels ; si la règle change, on sait où la modifier.

Règle métier : distinguer une entrée valide

Une quantité négative n’a pas de sens pour ce panier. Une première version peut retourner un code simple, mais un code numérique anonyme n’explique pas la nature de l’échec. À mesure que le programme grandit, représente les cas de réussite et d’erreur par un type nommé ou un pick.

pick ErreurPanier {
    Aucune,
    QuantiteNegative,
    PrixNegatif,
}

proc ligne_valide(ligne: &Ligne) -> bool {
    return ligne.prix_unitaire >= 0 and
           ligne.quantite >= 0;
}

On pourrait aussi imposer les conditions avec des clauses requires. Un contrat est approprié si un appel invalide indique une faute de programmation. Un résultat d’erreur explicite est plus adapté si l’entrée vient d’un utilisateur et que le programme doit continuer après l’avoir refusée.

Accumulation : calculer le total

Un panier simple peut être un tableau de taille fixe. Ce choix convient lorsque la capacité est connue et que le nombre de lignes fait partie des contraintes du domaine. Dans un programme réel où le nombre de lignes varie, choisissez une collection dont les règles d’allocation sont effectivement disponibles dans la bibliothèque et le backend que vous utilisez.

proc total_panier(lignes: &[3]Ligne) -> i64 {
    let mut total: i64 = 0;
    for index in 0..3 {
        set total = total + sous_total(&lignes[index]);
    }
    return total;
}

On parcourt les indices de zéro à trois, sans inclure trois dans la plage. C’est cohérent avec les trois positions 0, 1 et 2. Si la taille change, le code ne devrait pas répéter un 3 caché à plusieurs endroits : une constante ou une abstraction de collection adaptée.

Cas de vérification et comportement attendu

test "ligne avec prix nul et quantité nulle" {
    let ligne: Ligne = Ligne {
        prix_unitaire: 0,
        quantite: 0,
    };
    assert(sous_total(&ligne) == 0);
}

test "sous-total de deux articles" {
    let ligne: Ligne = Ligne {
        prix_unitaire: 6,
        quantite: 2,
    };
    assert(sous_total(&ligne) == 12);
}

Ces tests donnent un cas de frontière et un cas ordinaire. Les cas complémentaires pertinents comprennent plusieurs lignes, une quantité nulle et chacune des erreurs prévues. Les tests nommés servent aussi de documentation exécutable : quelqu’un qui découvre le module comprend les règles en parcourant les noms et les assertions.

Organisation des modules du projet

Quand le fichier devient trop long, le modèle peut se trouver dans un module, les règles de calcul dans un autre et le point d’entrée dans un troisième. Seuls devraient être exportés les types et procédures dont les autres modules ont besoin. Gardez les tests près du comportement qu’ils protègent et notez la version d’outil utilisée.

Une progression lisible sépare le modèle, le calcul d’une ligne, l’accumulation et le traitement des erreurs. Après chaque ajout, la commande de vérification disponible permet d’attribuer un diagnostic à la construction concernée. En cas de rejet, un petit fichier réduit facilite la comparaison avec les constructions déjà présentes dans le dépôt.

Sources Vitte pour approfondir cette étude

Les sources du dépôt permettent de comparer cette étude avec des exemples de conversion, d’analyse, de tableaux, de procédures et de modules. La grammaire décrit les formes prévues ; les tests montrent les cas traités par les différentes étapes ; les bibliothèques core détaillent les contrats de leurs abstractions. La page sur l’état du support relie ces sources aux capacités vérifiées du compilateur.

La grammaire décrit les formes prévues ; les tests du dépôt montrent les cas traités par les différentes étapes ; les bibliothèques core précisent leurs contrats ; la page État du support distingue ce qui est spécifié de ce qui fonctionne dans le compilateur. Le parcours a présenté les éléments essentiels de Vitte et la différence entre une règle documentée et une fonctionnalité confirmée. Le second cycle approfondit les invariants de boucle, les modèles d’états, les contrats et les modules.

Spécifier le projet avant de coder

La spécification du panier peut se résumer ainsi : « pour chaque ligne valide, le programme calcule le prix multiplié par la quantité, puis additionne les sous-totaux ». Elle doit également fixer l’acceptation d’une quantité nulle, le sens d’un prix négatif, l’unité des montants et la limite du total dans le type choisi.

Une ligne de prix 6 et quantité 2 produit un sous-total de 12. Si zéro est autorisé, une ligne contenant zéro produit zéro. Une valeur négative doit être refusée ou représentée par un état d’erreur explicite. Ces résultats donnent un sens concret aux règles métier et montrent pourquoi elles doivent être séparées de la simple multiplication.

Ordre de composition du calculateur

Responsabilité	Rôle dans le calculateur
Modèle	La forme Ligne rassemble le prix unitaire et la quantité.
Règle locale	sous_total multiplie les champs d’une ligne.
Validation	La règle métier distingue les valeurs permises des entrées refusées.
Accumulation	Le parcours additionne les sous-totaux avec un indice et une borne explicites.
Interface	Les modules séparent les déclarations internes de celles utilisées par d’autres fichiers.

Ce découpage donne des frontières où interpréter un diagnostic. Une erreur dans le prix unitaire appartient au modèle ou à la validation ; une valeur de ligne incorrecte renvoie au calcul local ; un total incomplet renvoie à l’accumulation ou à ses bornes.

Préparer les vérifications et reconnaître leurs limites

La matrice du projet confirme l’exécution de formes non génériques, de variantes pick, de tableaux fixes, de conditions et de boucles while dans des fixtures distinctes. Cette preuve ne signifie pas que leur combinaison dans le panier complet a déjà été exécutée. Le calculateur complet constitue une étude d’intégration : la preuve des composants séparés ne vaut pas automatiquement pour leur assemblage.

Le parcours initial utilise une boucle for sur plage et des déclarations test. Le backend natif audité n’a pas confirmé l’exécution de ces deux éléments sous cette forme. Une variante reposant sur while et sur un statut de retour se rapproche davantage du sous-ensemble runtime vérifié ; elle doit toutefois être lancée dans sa combinaison exacte avant d’être présentée comme une exécution confirmée.

Propriétés qui rendent le projet compréhensible

Le projet est prêt à être partagé lorsque quelqu’un peut comprendre ses entrées, ses résultats, les erreurs possibles et le modèle des données. Une fiche de vérification courte peut résumer les propriétés suivantes :

• Chaque procédure a un nom, des paramètres et un type de retour compréhensibles.
• Chaque règle métier a au moins un cas ordinaire et un cas de frontière.
• Chaque accès au tableau est précédé d’un raisonnement sur ses bornes.
• Chaque fonctionnalité dépendant du compilateur a une commande ou une mention explicite « non confirmée ».
• Les exports se limitent aux noms dont un autre module a besoin.

Calcul complet d’une ligne et du panier

Une ligne avec un prix unitaire de 6 et une quantité de 2 donne le sous-total 6 × 2 = 12. Une deuxième ligne à 4 pour 3 unités donne également 12. Une troisième ligne à 0 pour 5 unités donne 0. L’accumulation produit alors 12 + 12 + 0 = 24. Cette trace montre la composition de deux règles différentes : le calcul local à une ligne, puis la somme des lignes.

Cette séparation permet de localiser une erreur. Si le total est faux mais qu’un sous-total l’est déjà, le problème se trouve dans les données ou dans la multiplication. Si chaque sous-total est juste mais que la somme finale est fausse, l’accumulation, la borne ou la mise à jour mutable est à examiner. La procédure de ligne exprime une responsabilité stable ; la procédure de panier choisit les lignes qu’elle parcourt et rassemble les résultats.

Validité, erreurs et ordre de calcul

Le choix de traiter une valeur négative dépend de la règle métier. Le prix négatif peut être interdit, ou représenter un crédit si le domaine le définit ainsi ; la quantité négative peut être interdite ou être un retour de marchandises. Le type i64 permet de représenter les nombres négatifs, mais ne décide pas ce qu’ils signifient. La validation doit traduire la règle du panier, pas seulement la capacité du type.

Si une entrée invalide est une situation attendue, le résultat doit garder assez d’information pour que l’appelant explique le refus. Si elle indique une faute de programmation entre deux procédures internes, une précondition peut clarifier la responsabilité de l’appelant. Les limites numériques forment un autre cas : le produit prix × quantité, puis la somme des sous-totaux, peuvent dépasser i64. La borne doit être contrôlée au bon niveau, selon les opérations supportées par la cible.

Pourquoi la composition est séparée de la preuve

Le dépôt confirme les briques de formes, de variantes, de tableaux, de contrôles et de contrats dans des fixtures distinctes. Le calculateur présenté ici les assemble en une étude complète, mais cette combinaison n’est pas automatiquement couverte par l’exécution d’une fixture déjà existante. En particulier, le parcours initial emploie for sur une plage et des déclarations test, deux formes dont le chemin runtime n’est pas confirmé dans le backend natif audité.

Une version adaptée au sous-ensemble vérifié peut remplacer le parcours par while et contrôler le résultat au moyen d’un statut. La distinction entre modèle pédagogique et commande confirmée est une partie de la documentation technique : elle évite de transformer l’assemblage plausible de plusieurs syntaxes en affirmation de compilation. Les exemples de formes, tableaux et contrats liés sur cette page constituent des points de comparaison individuels avec une commande et un résultat publiés.

Règles d’erreur et atomicité du total

Si la troisième ligne d’un panier est invalide après deux lignes valides, le programme doit définir ce qu’il renvoie. Un total partiel de 24 pourrait être confondu avec un total complet. Une stratégie consiste à refuser le panier entier et à retourner une erreur portant l’indice ou la raison ; une autre peut ignorer les lignes invalides si cette règle est annoncée. Le choix appartient au domaine, mais le résultat doit distinguer total final et total partiel.

Cette décision influence l’ordre de calcul. Une validation de toutes les lignes avant l’accumulation sépare la détection d’erreurs du calcul. Une validation pendant le parcours peut arrêter immédiatement le traitement, à condition de ne pas exposer l’accumulateur partiel comme s’il était complet. Le type de retour devrait traduire cette distinction plutôt que la laisser dans une convention implicite.

Capacité fixe et croissance future

Le type [3]Ligne rend la capacité statique et la borne du parcours explicite. Il convient à un exemple de taille connue, à un protocole de longueur fixe ou à une représentation compacte. Un panier réel peut contenir un nombre variable de lignes ; ce besoin demande une collection qui gère l’allocation et l’extension selon des règles prises en charge par la bibliothèque et le backend.

Remplacer le tableau par une abstraction dynamique touche les coûts et les contrats : qui alloue, quand la capacité change, comment les références aux éléments restent valides, et quelles erreurs d’allocation peuvent survenir. La généralisation ne consiste donc pas à remplacer seulement la notation du type ; elle modifie les propriétés de mémoire et d’exécution du programme.