oracles-de-correction-ctoth

Oracles de correction

Choisissez une observation qui peut réfuter le comportement promis. Précisez ce qu'une vérification réussie laisse non testé : une comparaison de comptes, une vérification structurelle et un témoin de dépendance observent des propriétés différentes (Implémentation NoREC, Vérifications d'intégrité SQLite, Elle §4.3).

Dérivez la vérification à partir des limites réelles

Lisez la configuration activée, le producteur public et le contrat directeur de la cible. Identifiez les états de départ légaux, les préconditions des opérations, les erreurs autorisées et la limite promise : une opération, une instruction, une transaction, une récupération ou un historique observé. Dans SQLite, ABORT annule une instruction, tandis qu'une clé étrangère différée "n'est pas vérifiée tant que la transaction ne tente pas de COMMIT" (ABORT SQLite, clés étrangères différées). Interrogez les paramètres effectifs lorsque c'est possible ; le paramètre de clé étrangère de SQLite, par exemple, "est une opération nulle au sein d'une transaction" (clés étrangères SQLite).

Rédigez une observation candidate concrète avant de passer à l'échelle de la recherche :

• Promesse : le résultat ou l'effet exact interdit, avec sa citation contractuelle.
• Observation : le contenu, l'état ou le témoin réellement retourné qui distingue cette violation du comportement autorisé.
• Préconditions et angles morts : configuration prise en charge, état valide, informations omises et exécutions impossibles à distinguer.
• Preuve de rejeu : entrée et état initial, séquence d'opérations, configuration effective et observations brutes.

Il s'agit d'une convention de conception compacte, non d'un schéma obligatoire. Son but est d'exposer les informations perdues par la vérification proposée ; le modèle d'observation d'Elle montre pourquoi les dépendances cachées ne peuvent pas être récupérées en générant simplement plus d'historiques : les écritures aveugles sur les registres "détruisent l'histoire" (Elle §§3–4.3). Lisez les exemples de contrats pour des limites travaillées.

En JavaScript, un code de sortie de processus, le statut du test-runner ou une console propre est une telle observation : sa signification dépend du mode effectif, des écouteurs installés, de la configuration du test-runner et de la build. Avec un gestionnaire uncaughtExceptioninstallé, le processus Node "va sortir avec 0" sauf si le gestionnaire définit process.exitCode (Node process, uncaughtException). Lisez les canaux d'observation JavaScript pour les canaux Node, test-runner, React et Playwright.

Maintenez l'observation indépendante du comportement suspect

Tracez comment la valeur attendue ou l'invariant est obtenu. Identifiez le code partagé et les hypothèses qui pourraient permettre à la cible et au vérificateur de s'accorder sur la même réponse erronée. Préférez un modèle abstrait justifié, un invariant spécifié indépendamment ou une relation valide à un algorithme de production copié. Une seconde implémentation est une option : le test logique SQL de SQLite exécute des instructions sur plusieurs moteurs et vérifie "qu'ils obtiennent tous les mêmes réponses". Une relation sur le même moteur en est une autre : SQLite réexécute les suites de tests avec les optimisations désactivées, et NoREC de SQLancer compare une requête optimisée avec une requête non optimisée (Test SQLite §2, §9, Implémentation NoREC).

Mesurez l'information réellement comparée. Des comptes de lignes égaux n'établissent pas l'identité des lignes ; un integrity_check sain n'établit pas l'intégrité référentielle, car il "ne trouve pas les erreurs de clés étrangères". Conservez les vérifications partielles valides et ajoutez une observation complémentaire uniquement lorsque la garantie de la cible l'exige (Implémentation NoREC, Vérifications d'intégrité SQLite). Lisez observations partielles lorsque vous choisissez une référence, une normalisation ou un témoin.

Vérifiez les erreurs autorisées et leurs effets

Dérivez le post-état autorisé séparément du statut retourné. ABORT et FAIL de SQLite retournent tous deux une erreur de contrainte, mais ABORT annule l'instruction qui a échoué tandis que FAIL "n'annule pas les modifications antérieures de l'instruction SQL qui a échoué". Une assertion basée uniquement sur l'erreur peut manquer un effet erroné ; une assertion de rollback générique peut rejeter un comportement légal (Politiques de conflit SQLite).

Sélectionnez un observateur pour la promesse réelle, avec des préconditions valides. Pour les vérifications référentielles de SQLite, utilisez l'observation applicable de clé étrangère, le paramètre d'application effectif et la sémantique légale NULL ; ne substituez pas un résultat d'intégrité générique (Clés étrangères SQLite, foreign_key_check). Ce sont des contrats travaillés, pas des valeurs par défaut pour des API arbitraires.

Préservez le résultat et les limites de la vérification

Distinguer les propriétés évaluées des entrées rejetées, des erreurs attendues, des vérifications ignorées et des observations insuffisantes chaque fois que cette différence affecte la conclusion. NoREC ignore une comparaison lorsque l'un des comptes est sa valeur sentinelle -1 (par exemple, après une erreur de requête attendue) plutôt que de la compter comme une égalité, et signale une erreur inattendue comme un échec. La complétude d'Elle dépend des informations enregistrées, et "les observations sont rarement complètes" (Implémentation NoREC, Elle §4.3).

Utilisez harness-sensitivity pour établir que l'observation atteint et rejette une violation représentative justifiée indépendamment. Conservez le témoin brut pour evidence-based-triage : la propre documentation d'Elle recommande de "vérifier les anomalies rapportées à la main" plutôt que de traiter l'étiquette comme une autorité finale (README d'Elle). L'allocation générale de la recherche appartient à bugfinding-campaign.

Acheminez le raisonnement spécialisé choisi vers semantic-differential-testing, metamorphic-testing, linearizability-checking, transactional-history-testing, numerical-oracles, resource-complexity-testing ou liveness-testing ; cette compétence possède la décision contrat-observation. Lisez erreurs courantes pour les raccourcis trompeurs.

Retournez l'oracle utilisable

Retournez le producteur, la garantie citée, les préconditions effectives, l'observation exécutable et l'interprétation du résultat, avec une distinction travaillée autorisé/interdit. Indiquez ce qui reste inobservable et quelles preuves doivent survivre au rejeu. Une contradiction constatée ne soutient que la garantie et les hypothèses réellement vérifiées (Elle §§4.3 et 9).