Contrats et validation

Une signature dit déjà quelque chose

Dans proc doubler(valeur: i64) -> i64, le type annonce une entrée et une sortie numériques. Il ne dit pas si les valeurs négatives ont un sens, ni quelle relation doit exister entre l’entrée et la sortie. Un contrat peut préciser ces propriétés :

proc doubler(valeur: i64) -> i64
    requires valeur >= 0;
    ensures result == valeur * 2;
{
    return valeur * 2;
}

requires exprime une condition sur les paramètres avant l’appel. ensures décrit une propriété du résultat après l’exécution ; result désigne la valeur renvoyée. Le corps reste responsable de tenir cette promesse.

Écrire des engagements utiles

Une précondition doit préciser ce que l’appelant est tenu de fournir. Une postcondition doit préciser ce que l’appelant pourra ensuite supposer. Préférez une propriété simple à une formule qui répète tout le corps de la procédure.

Pour un calcul de prix après remise, le contrat précise notamment que le taux appartient à l’intervalle de 0 à 100, que le résultat respecte la règle métier par rapport au prix d’origine et que les prix négatifs suivent un traitement défini. Ces propriétés se traduisent ensuite en expressions vérifiables.

Évitez les contrats tautologiques. ensures result == result; est toujours vrai, mais n’apprend rien à l’appelant. Une bonne postcondition relie le résultat aux paramètres ou à une propriété métier.

Contrat ou erreur à traiter ?

Le choix dépend de la source de l’entrée et de la réaction attendue :

• Une précondition convient à un usage incorrect d’une procédure, quand l’appelant doit garantir que la condition est vraie.
• Une validation convient à une donnée venant d’un fichier, d’un utilisateur ou d’une autre source incertaine, lorsque le programme doit expliquer le refus et continuer.
• Un résultat représenté par pick convient quand réussite et échec sont deux résultats normaux que l’appelant doit distinguer.

Par exemple, une fonction interne peut exiger une quantité positive si tous ses appels contrôlent déjà cette règle. Une commande qui reçoit une quantité saisie au clavier doit la vérifier avant de l’envoyer au calcul ; elle ne doit pas considérer une entrée invalide comme une faute du langage.

Lire la preuve disponible dans le dépôt

Le fichier contrats.vit contient le contrat de doubler et appelle la procédure avec 21. Dans le dépôt audité, cet exemple passe par le chemin de compatibilité de la CLI :

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

Résultat confirmé : code de sortie 0. Cela établit l’exécution de ce cas valide dans ce chemin. Cela ne prouve pas à lui seul le comportement d’une violation de précondition dans chaque frontend. Pour ce détail, consultez la matrice de support Vitte et conservez la distinction entre une syntaxe décrite, une procédure vérifiée et un comportement runtime observé.

Décomposer une règle métier

Prenez la règle « doubler accepte une valeur positive ou nulle et renvoie son double ». Elle se décompose en trois affirmations :

1. valeur >= 0 est une condition d’entrée.
2. result == valeur * 2 est une propriété de sortie.
3. Le calcul dans le corps doit produire cette valeur pour toutes les entrées autorisées.

La troisième affirmation ne découle pas de l’écriture de la première et de la deuxième. Elle demande une vérification adaptée au projet. Pour les petites fonctions, comparez des cas simples ; pour des opérations plus délicates, ajoutez des tests de frontière et vérifiez les risques de dépassement numérique.

Séparer l’obligation de l’appelant de la promesse de la procédure

Un contrat a deux côtés. L’appelant doit respecter les conditions d’entrée. La procédure doit respecter sa postcondition si ces conditions sont satisfaites. Si vous ajoutez une condition qui dépend d’une donnée que l’appelant ne peut pas connaître, l’interface devient difficile à utiliser. Si votre postcondition affirme seulement une propriété déjà garantie par le type, elle n’ajoute peut-être rien.

Pour doubler, l’appelant fournit une valeur non négative ; la procédure promet le double. Le corps pourrait être remplacé plus tard par une autre implémentation sans changer le contrat, tant que la propriété reste vraie et que les limites numériques sont respectées.

Contrats et limites numériques

Une formule mathématique exacte ne tient pas toujours pour toutes les valeurs d’un entier machine. Le produit valeur * 2 peut dépasser la plage représentable. La précondition valeur >= 0 ne suffit donc pas à démontrer la postcondition pour toute valeur de type i64 si la plage maximale n’est pas également prise en compte.

Quand la borne dépend du type, vérifiezz la constante de limite fournie par la bibliothèque ou introduisez une condition qui empêche le dépassement selon les opérations prises en charge. Ne supposez pas que l’arithmétique s’enroule, se sature ou lève une erreur sans preuve dans la documentation de la cible.

Validation contrôlée ou précondition ?

Imaginez une quantité envoyée par un fichier de configuration. Si le fichier contient une quantité négative, le programme peut afficher une erreur compréhensible et demander une correction : la donnée doit être validée à la frontière. À l’inverse, si une procédure interne ne doit recevoir que des valeurs validées, un contrat peut signaler que l’un de ses appels viole la règle de conception.

La validation transforme une donnée incertaine en un état reconnu. Un contrat décrit la relation entre les procédures qui se font confiance dans le programme. Mélanger les deux rend l’erreur difficile à traiter : une saisie incorrecte ne devrait pas provoquer une panne interne inexpliquée.

Progresser sans surestimer l’outil

Le dépôt confirme l’exécution de contrats.vit par son chemin de compatibilité, avec un appel valide. La preuve ne décrit pas toutes les réactions possibles lors d’une violation, ni ne garantit que chaque frontend traite les clauses de la même manière. Documentez séparément le contrat souhaité et le comportement mesuré du compilateur.

La preuve disponible porte sur un appel valide. Le comportement d’une violation reste à établir séparément pour chaque chemin de compilation ; lorsque la CLI ne vérifie pas cette réaction, une validation explicite à la frontière de l’appel reste nécessaire.

Précondition et postcondition décrivent une relation

Une précondition restreint le domaine des appels autorisés. Une postcondition précise ce qui sera vrai du résultat lorsque l’appel respecte la précondition et que la procédure termine normalement. Pour doubler, valeur >= 0 décrit une partie du domaine ; result == valeur * 2 décrit une relation entre l’entrée et le résultat. La signature donne les types, tandis que le contrat ajoute les propriétés qui ne sont pas exprimées par ces types seuls.

Une postcondition utile est plus informative que le corps recopié sous une autre forme. Elle peut rester stable même si l’algorithme change. Si l’implémentation passe d’une multiplication à une autre méthode équivalente, la promesse demeure la même. À l’inverse, une propriété tautologique telle que result == result n’impose aucun lien avec les paramètres ou le domaine métier.

La frontière d’entrée transforme une donnée incertaine

Une donnée lue depuis un fichier, une option de ligne de commande ou une interface utilisateur est incertaine avant validation. Le programme ne peut pas présumer que l’appelant a respecté ses contraintes. Une validation à cette frontière transforme l’entrée en une valeur reconnue ou en un état d’erreur qui peut être affiché et traité. Une précondition convient davantage aux appels internes dont les responsabilités sont établies par la conception du programme.

La distinction a une conséquence pratique : un contrat violé peut signaler un défaut de programmation, tandis qu’une entrée invalide peut être une situation ordinaire. Les deux peuvent partager une expression logique comme quantite >= 0, mais leur réaction attendue diffère. La première peut interrompre ou diagnostiquer un chemin incorrect ; la seconde doit souvent permettre à l’application de continuer après un message compréhensible.

La preuve doit tenir compte des entiers machine

La propriété mathématique « le double de n vaut n + n » ne garantit pas que le résultat tient dans i64. Une valeur positive proche de la borne supérieure peut dépasser la représentation. Le contrat doit intégrer la limite numérique si l’opération s’effectue dans ce type, et le comportement exact en cas de dépassement dépend de la cible et du runtime.

Dans le dépôt, l’exemple contrats.vit s’exécute avec une entrée valide et renvoie un statut réussi par le chemin de compatibilité documenté. Cela confirme ce cas précis ; cela ne démontre pas comment une violation est signalée dans chaque frontend ni que toute valeur satisfaisant la précondition simplifiée peut être doublée sans dépassement. La portée exacte de la preuve fait donc partie de l’explication du contrat.

Validité, sécurité et confiance entre couches

Un contrat formalise la confiance entre une procédure et ses appelants. La couche qui reçoit une donnée externe ne peut pas s’appuyer sur une promesse non encore vérifiée ; elle est responsable de la validation. Une procédure interne peut ensuite recevoir une valeur déjà validée et se concentrer sur son invariant. Cette organisation évite que chaque calcul répète toute la validation tout en gardant une frontière sûre au point d’entrée.

Un contrat trop strict rejette des valeurs que l’API pourrait traiter ; un contrat trop faible autorise des appels pour lesquels le corps ne peut pas tenir sa promesse. La précision demande de connaître le domaine, les valeurs limites et les opérations numériques. Des clauses lisibles sont préférables à une formule dense que l’appelant ne peut pas interpréter.

Contrat vérifié et contrat supposé

Une spécification dans le code indique l’intention. Une analyse statique peut vérifier certaines propriétés ; un runtime peut évaluer une clause ; des tests peuvent observer des appels particuliers. Ces formes de preuve ne sont pas équivalentes. Un contrat accepté par l’analyseur n’est pas nécessairement prouvé mathématiquement, et un appel valide exécuté ne montre pas le traitement d’une violation.

Pour Vitte, l’exemple lié sur cette page confirme un appel valide par le chemin de compatibilité disponible. Les réactions exactes aux violations restent dépendantes du frontend et de sa génération. La documentation de l’application doit donc distinguer la garantie de conception, la vérification du compilateur et les comportements effectivement observés.