ctoth/correctness-oracles

Korrektheits-Orakel

Wähle eine Beobachtung, die das versprochene Verhalten widerlegen kann. Lege fest, was ein erfolgreicher Test ungetestet lässt: Ein Vergleich von Anzahlen, eine strukturelle Prüfung und ein Abhängigkeitszeuge beobachten unterschiedliche Eigenschaften (NoREC-Implementierung, SQLite-Integritätsprüfungen, Elle §4.3).

Leite die Prüfung von der tatsächlichen Grenze ab

Lies die aktivierte Konfiguration des Ziels, den öffentlichen Produzenten und den maßgeblichen Vertrag. Identifiziere erlaubte Startzustände, Operationsvorbedingungen, erlaubte Fehler und die versprochene Grenze: eine Operation, Anweisung, Transaktion, Wiederherstellung oder beobachtete Historie. In SQLite macht ABORT eine Anweisung rückgängig, während eine zurückgestellte Fremdschlüsselbedingung "erst beim COMMIT der Transaktion geprüft wird" (SQLite ABORT, zurückgestellte Fremdschlüssel). Frage wann immer möglich effektive Einstellungen ab; die Fremdschlüsseleinstellung von SQLite beispielsweise "ist innerhalb einer Transaktion wirkungslos" (SQLite foreign_keys).

Schreibe eine konkrete Kandidatenbeobachtung, bevor du die Suche skalierst:

• Versprechen: das exakte verbotene Ergebnis oder der exakte verbotene Effekt, mit Vertragszitat.
• Beobachtung: tatsächlicher zurückgegebener Inhalt, Zustand oder Zeuge, der diesen Verstoß von erlaubtem Verhalten unterscheidet.
• Vorbedingungen und blinde Flecken: unterstützte Konfiguration, gültiger Zustand, ausgelassene Informationen und nicht unterscheidbare Ausführungen.
• Wiederholungsnachweis: Eingabe und Ausgangszustand, Operationssequenz, effektive Konfiguration und rohe Beobachtungen.

Dies ist eine kompakte Designkonvention, kein erforderliches Schema. Ihr Zweck ist es, Informationen aufzudecken, die durch die vorgeschlagene Prüfung verloren gehen; Elles Beobachtungsmodell zeigt, warum verborgene Abhängigkeiten nicht allein durch das Erzeugen weiterer Historien wiederhergestellt werden können: blinde Register-Schreibvorgänge "zerstören die Historie" (Elle §§3–4.3). Lies Vertragsbeispiele für ausgearbeitete Grenzen.

In JavaScript ist ein Prozess-Exit-Code, Test-Runner-Status oder eine saubere Konsole eine solche Beobachtung: Ihre Bedeutung hängt vom effektiven Modus, installierten Listenern, der Runner-Konfiguration und dem Build ab. Mit einem installierten uncaughtException-Handler wird der Node-Prozess "mit 0 beenden", es sei denn, der Handler setzt process.exitCode (Node-Prozess, uncaughtException). Lies JavaScript-Beobachtungskanäle für Node-, Test-Runner-, React- und Playwright-Kanäle.

Halte die Beobachtung unabhängig vom verdächtigen Verhalten

Verfolge, wie der erwartete Wert oder die Invariante gewonnen wird. Identifiziere gemeinsamen Code und Annahmen, die dazu führen könnten, dass Ziel und Prüfer sich auf die gleiche falsche Antwort einigen. Bevorzuge ein gerechtfertigtes abstraktes Modell, eine unabhängig spezifizierte Invariante oder eine gültige Relation gegenüber einem kopierten Produktionsalgorithmus. Eine zweite Implementierung ist eine Option: Der SQL-Logiktest von SQLite führt Anweisungen gegen mehrere Engines aus und prüft, "dass sie alle die gleichen Antworten erhalten". Eine gleich-Engine-Relation ist eine andere: SQLite führt Suiten mit deaktivierten Optimierungen erneut aus, und SQLancers NoREC vergleicht eine optimierte Abfrage mit einer nicht optimierten (SQLite-Tests §2, §9, NoREC-Implementierung).

Messe die tatsächlich verglichenen Informationen. Gleiche Zeilenanzahlen begründen keine Zeilenidentität; eine gesunde integrity_check begründet keine referentielle Integrität, da sie "keine FOREIGN KEY Fehler findet". Bewahre gültige Teilprüfungen und füge eine komplementäre Beobachtung nur dann hinzu, wenn es die Zielgarantie erfordert (NoREC-Implementierung, SQLite-Integritätsprüfungen). Lies Teilbeobachtungen bei der Wahl einer Referenz, Normalisierung oder eines Zeugen.

Prüfe erlaubte Fehler und ihre Auswirkungen

Leite den erlaubten Nachzustand getrennt vom zurückgegebenen Status ab. Sowohl ABORT als auch FAIL von SQLite geben einen Constraint-Fehler zurück, aber ABORT macht die fehlgeschlagene Anweisung rückgängig, während FAIL "vorherige Änderungen der fehlgeschlagenen SQL-Anweisung nicht rückgängig macht". Eine reine Fehlerbehauptung kann einen falschen Effekt übersehen; eine pauschale Rollback-Behauptung kann legales Verhalten ablehnen (SQLite-Konfliktstrategien).

Wähle einen Beobachter für das tatsächliche Versprechen mit gültigen Vorbedingungen. Verwende für referentielle Prüfungen von SQLite die anwendbare Fremdschlüsselbeobachtung, die effektive Durchsetzungseinstellung und legale NULL-Semantiken; ersetze kein generisches Integritätsergebnis (SQLite Fremdschlüssel, foreign_key_check). Dies sind ausgearbeitete Verträge, keine Standardeinstellungen für beliebige APIs.

Bewahre das Ergebnis und die Grenzen der Prüfung

Unterscheide bewertete Eigenschaften von abgelehnten Eingaben, erwarteten Fehlern, übersprungenen Prüfungen und unzureichenden Beobachtungen, wann immer dieser Unterschied die Schlussfolgerung beeinflusst. NoREC überspringt einen Vergleich, wenn einer der Zähler sein -1-Sentinel ist (z. B. nach einem erwarteten Abfragefehler), anstatt ihn als Gleichheit zu werten, und meldet einen unerwarteten Fehler als Fehlschlag. Elles Vollständigkeit hängt von den aufgezeichneten Informationen ab, und "Beobachtungen sind selten vollständig" (NoREC-Implementierung, Elle §4.3).

Verwende harness-sensitivity, um zu belegen, dass die Beobachtung einen repräsentativen, unabhängig begründeten Verstoß erreicht und ablehnt. Bewahre den rohen Zeugen für evidence-based-triage auf: Elles eigene Dokumentation empfiehlt, "gemeldete Anomalien von Hand zu überprüfen", anstatt die Kennzeichnung als endgültige Autorität zu behandeln (Elle README). Die allgemeine Suchzuweisung gehört zu bugfinding-campaign.

Leite die gewählte spezialisierte Argumentation an semantic-differential-testing, metamorphic-testing, linearizability-checking, transactional-history-testing, numerical-oracles, resource-complexity-testing oder liveness-testing weiter; dieses Skill besitzt die Entscheidung vom Vertrag zur Beobachtung. Lies häufige Fehler für irreführende Abkürzungen.

Gib das verwendbare Orakel zurück

Gib den Produzenten, die zitierte Garantie, die effektiven Vorbedingungen, die ausführbare Beobachtung und die Ergebnisinterpretation mit einer ausgearbeiteten Unterscheidung erlaubt/verboten zurück. Gib an, was nicht beobachtbar bleibt und welche Beweise eine Wiederholung überstehen müssen. Ein bezeugter Widerspruch stützt nur die Garantie und die Annahmen, die tatsächlich geprüft wurden (Elle §§4.3 und 9).