Votre code correspond-il à votre spec?

Kiro est un IDE agentif qui a introduit le développement piloté par les spécifications (Spec Driven Development, SDD) lors de son lancement en juillet. Avec le SDD, l'agent de Kiro rédige une spécification complète de votre logiciel avant d'écrire du code. Cela vous permet d'itérer avec l'agent et de vérifier que vous avez bien saisi toutes les exigences de votre application avant de la développer. Kiro traduit ensuite votre document d'exigences en une « spécification exécutable » qu'il utilise pour vérifier si le code généré respecte la spécification. Kiro utilise ces spécifications exécutables pour tester votre programme, à l'aide d'une technique appelée test basé sur les propriétés, que nous croyons plus efficace pour trouver des bogues.

Lorsque vous utilisez Kiro, il génère du code à partir d'un Spec. Comment savoir si le code fait vraiment ce que le Spec indique qu'il devrait faire? Kiro et d'autres outils de génération de code par IA générative utilisent des tests unitaires générés automatiquement pour aider à répondre à cette question. Kiro génère des tests unitaires en même temps que le code, et s'assure que le code les réussit. Mais il y a un problème de l'œuf et de la poule. Comment savoir si les tests unitaires reflètent bien le comportement décrit dans la spécification? Nous devons examiner chaque test et déterminer 1/ à quelle(s) exigence(s) de la spécification le test peut s'appliquer, et 2/ si le comportement prescrit dans le test correspond à la spécification. Ces deux étapes peuvent être fastidieuses et sujettes à erreur.

Il s'avère que, dans certains cas, nous pouvons faire mieux en utilisant des tests basés sur les propriétés, plutôt que des tests unitaires. Les tests unitaires sont essentiellement des tests « basés sur des exemples », composés de paires entrée/sortie uniques. Chacun affirme que, pour un exemple précis, votre système se comporte d'une certaine façon. En revanche, un test basé sur les propriétés (ou simplement, test de propriété) vérifie qu'une propriété est vraie pour le comportement du système, c'est-à-dire qu'elle tient pour une large (potentiellement infinie) gamme d'entrées. C'est cette universalité qui donne aux tests de propriétés leur puissance. Étant donné certains tests de propriétés, nous générons aléatoirement de nombreuses entrées afin de les tester. Si le test de propriété retourne un jour faux, nous avons trouvé un contre-exemple qui viole la propriété. Cela représente probablement un bogue dans le programme testé (mais il pourrait aussi s'agir d'un bogue dans la définition de la propriété, ou dans la spécification originale, ce qui est également utile à découvrir). Kiro peut utiliser cet exemple pour corriger le code jusqu'à ce qu'il soit correct.

Le test basé sur les propriétés a été inventé il y a plus de deux décennies pour le langage de programmation Haskell, dans un cadre appelé QuickCheck. Il a évolué et mûri au fil du temps. Les tests de propriétés se marient très bien avec le développement piloté par les spécifications, tel que pratiqué par Kiro, car les exigences de la spécification expriment souvent directement des propriétés, et ces propriétés peuvent être testées à l'aide de tests basés sur les propriétés. En un sens, les propriétés sont une autre représentation (de parties) de votre spécification. Avec les tests basés sur les propriétés, nous obtenons une « spécification exécutable » — en d'autres termes : une version de la spécification que nous pouvons exécuter. La spécification exécutable composée de tests basés sur les propriétés est facilement liée aux exigences textuelles, ce qui nous donne l'assurance que, tant que les tests de propriétés réussissent, notre code fait ce que les exigences indiquent qu'il devrait faire.

À titre d'exemple, imaginons que nous écrivons un petit simulateur de feux de circulation en Python. Kiro créera une spécification avec un document d'exigences composé de critères d'acceptation. Un des critères d'acceptation pourrait ressembler à ceci :

Ce critère exprime une condition importante pour un feu de circulation : que deux directions ne sont jamais vertes en même temps. Voici ce critère d'acceptation transformé en une propriété textuelle.

Remarquez que cette propriété commence par les mots « for any » (pour tout). C'est une propriété parce qu'elle parle d'une gamme d'entrées et de comportements, et non de la description du traitement d'une seule entrée exemple. Kiro prend ce texte de propriété et le transforme en test basé sur les propriétés, c'est-à-dire une spécification exécutable. Kiro relie les deux, en nous permettant de naviguer directement de notre spécification textuelle vers le test qui vérifie cette propriété.

Kiro traduit les propriétés textuelles en tests basés sur les propriétés écrits à l'aide d'un cadre appelé Hypothesis, que nous verrons plus en détail plus loin. Le code de notre propriété de feu de circulation est donné ci-dessous. Nous pouvons lire ce code et voir qu'il vérifie effectivement la propriété qui nous intéresse. Il vérifie d'abord que nous partons d'un état nominal. Ensuite, il parcourt chaque opération de la séquence d'opérations, les applique, et vérifie que l'on ne voit jamais qu'un seul feu vert.

Ce qui est formidable avec ce test de propriété, c'est qu'il teste directement l'exigence dont nous sommes partis. Cela signifie que si nous utilisons suffisamment d'entrées, nous obtenons l'assurance que l'exigence est respectée. Plus important encore, le corollaire est également vrai : le programme est incorrect s'il existe une entrée qui fait échouer cette fonction. Kiro tirera grandement parti de ce fait.

Un élément clé du test de propriétés est de générer aléatoirement une gamme diversifiée d'entrées avec lesquelles exécuter un test de propriété. Dans notre exemple, l'entrée clé est la list d'opérations passée à test_safety_invariant_at_most_one_green. Nous discuterons de la génération d'entrées dans le contexte de cet exemple dans la prochaine section. La génération automatisée d'entrées offre un avantage clé par rapport aux tests unitaires. Chaque fois que quelqu'un écrit des tests unitaires (qu'il s'agisse d'un modèle ou d'un humain), il essaiera de tenir compte des cas limites, mais il est limité par ses propres biais internes. En utilisant la génération aléatoire, nous pouvons souvent découvrir des cas limites et des interactions entre composants qui sont souvent oubliés.

La littérature sur l'exactitude des programmes montre qu'il existe des « formes » courantes de propriétés qui tendent à revenir. Kiro connaît ces formes et les recherche lors de la génération de propriétés. Par exemple, une propriété courante des structures de données, comme les arbres de recherche binaires, est qu'elles maintiennent un certain invariant d'exécution. Nous pouvons écrire une propriété pour vérifier que les opérations individuelles maintiennent l'invariant.

Une autre forme courante de propriété est le « aller-retour », dans lequel une certaine séquence d'opérations vous redonne la valeur de départ. Cette propriété est particulièrement utile pour les analyseurs (parsers) et les sérialiseurs.

Souvent, pour les API Web, nous voulons que les opérations de suppression soient « idempotentes », ce qui signifie que répéter une action deux fois a le même effet que de la faire une seule fois.

Pour plus d'informations sur la conception de propriétés par vous-même, nous vous recommandons l'article de blogue suivant : Choosing Properties for Property-Based Testing, et les articles How To Specify it [PDF].

Pour tester des propriétés, nous avons besoin de valeurs d'entrée concrètes. Pour obtenir de nombreuses (des centaines de) valeurs diversifiées et réduire l'impact des biais, les cadres de PBT utilisent des « générateurs », qui sont des fonctions qui prennent une forme d'aléatoire et produisent des valeurs d'entrée d'un type donné. Les utilisateurs de cadres de test basé sur les propriétés précisent quels générateurs d'entrées utiliser lors de l'exécution de tests de propriétés particuliers. Kiro fait cela pour nous pour les tests de propriétés qu'il génère. Les cadres de PBT tels qu'Hypothesis sont fournis avec un ensemble de générateurs pour les types courants, que vous pouvez utiliser comme blocs de construction pour créer des générateurs plus complexes. Le cadre Hypothesis appelle ses générateurs des strategies, et les stocke souvent dans la variable st. Voici quelques exemples de stratégies pour générer des entiers.

Hypothesis est également fourni avec des stratégies plus complexes pour des types de données personnalisés.

Nous pouvons également construire des stratégies complexes à partir de stratégies plus petites. Par exemple, la stratégie lists prend une autre stratégie en argument, et construit des listes d'éléments générés par cette dernière.

À partir d'aujourd'hui, Kiro rédige pour vous des tests basés sur les propriétés, à la fois le code de vérification des propriétés et les générateurs, afin de tester vos exigences. Pour en revenir à notre exemple de feu de circulation, Kiro ne se limite pas à générer le code de vérification des propriétés que nous avons vu plus haut, il ajoute aussi les annotations @given au-dessus de la méthode, en listant les deux stratégies Hypothesis que nous voulons utiliser.

Voici la stratégie que Kiro a écrite pour notre propriété. Ce code utilise le cadre de stratégies Hypothesis pour construire une stratégie sur des séquences de transitions de feux de circulation. Nous pouvons voir la stratégie référencer d'autres stratégies que Kiro a écrites, telles que signal_state_strategy, ce qui permet le partage de code entre plusieurs tests de propriétés.

Ce test s'intègre nativement avec pytest, le cadre de test standard pour Python. Lorsque pytest est exécuté, Hypothesis génère 100 cas de test, et s'assure qu'ils réussissent tous la propriété.

Pour la qualité des tests, il est important que les stratégies de génération d'entrées produisent effectivement une variété d'entrées. Nous pouvons évaluer notre performance à cet égard en examinant ces entrées, ainsi que le code couvert lors de leur exécution, à l'aide d'un outil appelé Tyche. Voici quelques exemples d'entrées trouvées par le générateur, que Tyche nous présente :

Voici une visualisation que Tyche produit pour montrer le code exécuté par notre test basé sur les propriétés. On peut voir que même après 50 essais, nous explorons encore de nouveaux chemins de code.

Une mise en garde à propos de la couverture de code : bien qu'il s'agisse d'une mesure extrêmement courante pour évaluer l'efficacité d'une suite de tests, elle n'est pas l'arbitre ultime de la qualité des tests. Couvrir (c'est-à-dire exécuter) une ligne de code ne signifie pas que nous avons épuisé tous les comportements possibles sur cette ligne. Le test basé sur les propriétés ne peut pas garantir que votre programme est exempt de bogues, car il ne s'agit pas d'une technique exhaustive. Il pourrait toujours exister un contre-exemple que le test basé sur les propriétés échoue à trouver. Cependant, nous croyons que le test basé sur les propriétés est un outil plus efficace que le test traditionnel basé sur des exemples pour trouver des bogues, qu'il fait un meilleur travail pour relier vos spécifications et vos tests, et qu'il franchit l'étape cruciale de formuler le problème de l'exactitude des programmes en termes de spécifications concrètes et exécutables.

Avant de terminer cet article, nous voulons parler d'une dernière caractéristique du test basé sur les propriétés qui est vraiment utile : la réduction (shrinking). Lorsqu'un test de propriété échoue, vous obtenez une entrée qui fait échouer la propriété, c'est-à-dire un contre-exemple. Idéalement, vous aimeriez obtenir une entrée minimale, un petit exemple qui démontre le cœur du problème ayant fait échouer le test. Un contre-exemple géant contient probablement des données superflues qui n'ont rien à voir avec le problème, alors qu'un exemple minimal vous aide (et probablement aussi l'agent Kiro) à identifier la véritable faute dans le programme et à la corriger. La plupart des cadres de test basé sur les propriétés tentent de vous fournir un exemple minimal grâce à un processus appelé « réduction » (shrinking). Voyons comment cela fonctionne.

Imaginons que nous implémentons un ensemble (set) appuyé sur un arbre de recherche. Nous aurions probablement la propriété suivante :

En exécutant ce test, nous pourrions obtenir une sortie comme celle-ci :

Mais ce n'était en fait pas le premier contre-exemple que Hypothesis a trouvé. En examinant les journaux d'Hypothesis, le premier contre-exemple ayant échoué était en réalité le suivant :

Ce serait un cas beaucoup plus pénible à déboguer! La réduction simplifie systématiquement l'entrée en échec tout en vérifiant qu'elle déclenche toujours l'échec. Dans notre exemple, Hypothesis a retiré les nœuds inutiles, réduit les valeurs entières et simplifié la structure de l'arbre jusqu'à trouver le cas minimal : deux arbres à un seul nœud, contenant tous deux la valeur 0. Cela révèle le problème de fond — l'opération d'union ne gère pas correctement les valeurs en double — sans le bruit d'une structure d'arbre complexe.

Lorsque Kiro génère des tests de propriétés, il tire parti des capacités de réduction du cadre de PBT sous-jacent. Cela signifie que lorsqu'un test de propriété échoue pendant le développement, vous obtenez un contre-exemple minimal et exploitable qui rend le débogage beaucoup plus facile. L'agent peut utiliser cet exemple minimal pour comprendre plus facilement la cause profonde et proposer une correction, créant ainsi une boucle de rétroaction étroite entre la spécification, le test et l'implémentation. Lorsque Kiro constate que l'implémentation pourrait être correcte mais qu'elle est en désaccord avec la spécification, ou si le code généré par l'IA semble fondamentalement erroné d'une manière non triviale, Kiro signale la situation au développeur afin qu'il fasse un choix : corriger le code, corriger le Spec, ou corriger le PBT. Cela permet de combiner le jugement humain avec l'IA et les PBT pour mieux aligner l'implémentation sur l'intention du développeur.

L'intégration du test basé sur les propriétés par Kiro représente un changement dans notre façon de penser l'exactitude des tâches de programmation avec l'IA, passant de la vérification d'exemples individuels à la validation de propriétés universelles sur des espaces d'entrées entiers. En traduisant automatiquement les spécifications en langage naturel en propriétés exécutables et en générant des cas de test complets, Kiro crée une puissante boucle de rétroaction qui aide à la fois les agents d'IA et les développeurs humains à créer des logiciels plus fiables. Cette approche non seulement trouve des bogues que les tests traditionnels manquent, mais elle maintient aussi un lien clair et traçable entre les exigences et les tests qui les valident. Bien que le PBT ne puisse pas garantir l'absence de tous les bogues, il fournit une preuve d'exactitude nettement plus solide que le test basé sur des exemples seul, ce qui en fait un outil essentiel pour le développement piloté par les spécifications.

Pour plus d'informations sur les grands modèles de langage et le test basé sur les propriétés, veuillez consulter les articles de recherche suivants :

• QuickCheck
• Can LLMs write good PBTs
• Agentic PBT
• Use Property-Based Testing to Bridge LLM Code Generation and Validation
• Tyche [PDF]

Téléchargez Kiro, et essayez le test basé sur les propriétés avec les specs.