Exactitude avec les tests basés sur les propriétés

« L'exactitude des Specs » aide à répondre à une question fondamentale : votre implémentation fait-elle réellement ce que vous avez spécifié? Lorsque l'IA génère du code, comment savoir s'il correspond à votre intention?

La plupart des tests aujourd'hui sont basés sur des exemples : chaque test met en place un cas concret avec des entrées précises et vérifie un seul résultat attendu. Vous écrivez chaque cas à la main, donc votre couverture se limite aux exemples que vous (ou l'IA) avez pensé à inclure. Les tests basés sur les propriétés (PBT) renversent cette approche. Plutôt que de lister des exemples, vous énoncez une règle générale qui doit toujours être vraie, et l'outil génère des centaines ou des milliers d'entrées aléatoires pour tenter de la violer.

Vous pourriez voir cette même idée appelée fuzzing ou test génératif. Les termes sont largement interchangeables - le fuzzing est né de la sécurité et de la recherche de plantages, tandis que les tests basés sur les propriétés mettent l'accent sur l'exactitude logique fine - mais les trois génèrent automatiquement de nombreuses entrées et vérifient qu'une propriété se maintient.

Il s'agit d'une étape vers un changement fondamental dans la façon dont nous concevons l'exactitude avec l'IA, passant de la vérification d'exemples individuels à la validation de propriétés universelles sur des espaces d'entrées complets. Les tests unitaires traditionnels ne vérifient que des exemples précis, et quiconque les écrit - humain ou IA - est limité par ses propres biais. En traduisant automatiquement les spécifications en langage naturel en propriétés exécutables et en générant des cas de test à partir de celles-ci, Kiro crée une boucle de rétroaction qui aide à la fois les agents 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 maintient aussi un lien clair et traçable entre vos exigences et les tests qui les valident.

Une propriété est une affirmation universelle sur la façon dont votre système devrait se comporter. Les propriétés expriment les invariants et les contrats qui devraient toujours être vrais dans votre système, indépendamment des données précises impliquées.

Pour tout ensemble d'entrées où certaines conditions préalables sont respectées, un comportement attendu est vrai.

Dans l'univers des spécifications Kiro, cela correspond très bien à nos exigences EARS :

« Pour tout utilisateur authentifié et toute annonce active, l'utilisateur peut consulter cette annonce. » Cela capture une règle générale sur le comportement du système qui doit se maintenir dans tous les scénarios valides.

Prenons l'exemple d'une application de vente de voitures :

• Test traditionnel : L'utilisateur ajoute la voiture no 5 à ses favoris, la voiture no 5 apparaît dans sa liste
• Test basé sur les propriétés : Pour tout utilisateur et toute voiture, QUAND l'utilisateur ajoute la voiture à ses favoris, LE Système DOIT l'afficher dans sa liste

Le PBT teste automatiquement ceci avec l'utilisateur A ajoutant la voiture no 1, l'utilisateur B ajoutant la voiture no 500, des utilisateurs ayant des caractères spéciaux dans leur nom, des voitures avec différents statuts, et des centaines d'autres combinaisons - repérant les cas limites et vérifiant que l'implémentation correspond à l'intention.

Tout au long de ce processus, le PBT sonde pour trouver des contre-exemples grâce au rétrécissement - presque comme une équipe rouge qui essaie de briser votre code. Lorsqu'une entrée aléatoire déclenche un échec, cette entrée est souvent volumineuse et bruyante (un nom d'utilisateur de 200 caractères, une liste de 1 000 voitures). Le rétrécissement la réduit automatiquement à la plus petite entrée qui reproduit encore l'échec - souvent une simple chaîne vide ou une liste à deux éléments - afin que la cause profonde soit évidente plutôt qu'enfouie. Lorsqu'il trouve une violation, Kiro peut automatiquement mettre à jour votre implémentation ou proposer des options pour corriger la spec, l'implémentation ou le test lui-même.

Bien qu'il ne s'agisse pas de vérification formelle, le PBT fournit des preuves d'exactitude pour des scénarios que vous n'écririez jamais manuellement - montrant si votre implémentation se comporte réellement selon ce que vous avez défini.

Les tests basés sur les propriétés font gagner du temps et augmentent la confiance dans le code généré par l'IA, car :

• Une seule propriété génère automatiquement de nombreux cas de test, vous n'êtes donc pas limité aux exemples que vous ou l'IA avez pensé à écrire à la main.
• Les propriétés sont plus abstraites et plus durables que des exemples précis, ce qui rend les tests plus faciles à maintenir et plus résilients aux changements dans l'implémentation.
• Les entrées aléatoires exercent des cas que vous ne testeriez pas délibérément, y compris les valeurs vides, les conditions limites et les caractères inhabituels.
• Exercer le système plus rigoureusement fait ressortir des bogues rares avant qu'ils n'atteignent la production.
• Définir les propriétés qu'une spec doit garantir, avant l'exécution de tout test, force l'exigence à être précise et plus facile à raisonner.

Les tests basés sur les propriétés ont aussi des limites :

• Ils fournissent des preuves d'exactitude, pas une démonstration formelle. Il ne s'agit pas de vérification formelle, donc des tests réussis augmentent la confiance mais ne garantissent pas l'absence de bogues.
• Identifier et définir des propriétés utiles demande du travail. Une propriété trop faible, ou qui énonce le mauvais invariant, passera le test alors que le comportement réel est toujours erroné.
• Toutes les exigences ne se traduisent pas proprement en propriété. Les exigences qui dépendent fortement de services externes ou d'un comportement non déterministe peuvent nécessiter du mocking, ou être mieux couvertes par des tests basés sur des exemples.

Kiro intègre les tests basés sur les propriétés tout au long du flux de travail des Specs, des exigences jusqu'à la validation de l'implémentation.

Kiro extrait les propriétés de vos exigences au format EARS (p. ex. « LE Système DOIT permettre aux utilisateurs authentifiés de consulter les annonces de voitures actives »), détermine lesquelles peuvent être testées logiquement, puis génère des centaines ou des milliers de cas de test aléatoires lorsque vous choisissez de les exécuter.

Dans la phase de conception, Kiro extrait les propriétés de vos exigences et génère des cas de test. C'est la première étape du flux de travail, où Kiro analyse vos exigences et détermine les propriétés qui peuvent être testées.

Chargement de l'image...

Survoler une propriété révèle son lien avec l'exigence d'origine et la tâche associée.

Chargement de l'image...

Dans la phase d'exécution, Kiro exécute les cas de PBT générés contre votre implémentation. Remarque : les PBT sont facultatifs par défaut afin que vous puissiez d'abord vous concentrer sur votre implémentation principale. Une fois qu'un test de propriété est exécuté, vous pouvez voir la référence au code généré.

Chargement de l'image...

Lorsqu'un test de propriété échoue, Kiro repère le scénario d'échec précis et le fait ressortir pour examen.

Chargement de l'image...

Vous pouvez ensuite clavarder avec Kiro pour comprendre l'échec et déterminer la correction appropriée - qu'il s'agisse de mettre à jour l'implémentation, d'ajuster le test ou de raffiner l'exigence elle-même.

Chargement de l'image...