Oráculos de corrección
Elija una observación que pueda refutar el comportamiento prometido. Especifique qué deja sin probar una comprobación exitosa: una comparación de conteos, una comprobación estructural y un testigo de dependencias observan propiedades diferentes (implementación de NoREC, comprobaciones de integridad en SQLite, Elle §4.3).
Derive la comprobación a partir del límite real
Lea la configuración habilitada del objetivo, el productor público y el contrato rector. Identifique los estados iniciales legales, las precondiciones de operación, los errores permitidos y el límite prometido: una operación, sentencia, transacción, recuperación o historial observado. En SQLite, ABORT deshace una sentencia, mientras que una clave foránea diferida "no se verifica hasta que la transacción intenta hacer COMMIT" (ABORT en SQLite, claves foráneas diferidas). Consulte la configuración efectiva cuando sea posible; la configuración de claves foráneas en SQLite, por ejemplo, "es un no-op dentro de una transacción" (foreign_keys en SQLite).
Escriba una observación candidata concreta antes de escalar la búsqueda:
- Promesa: el resultado o efecto exacto prohibido, con su cita contractual.
- Observación: el contenido devuelto real, el estado o el testigo que distingue esa violación del comportamiento permitido.
- Precondiciones y puntos ciegos: configuración soportada, estado válido, información omitida y ejecuciones indistinguibles.
- Evidencia de repetición: entrada y estado inicial, secuencia de operaciones, configuración efectiva y observaciones sin procesar.
Es una convención de diseño compacta, no un esquema obligatorio. Su propósito es exponer la información que se pierde con la comprobación propuesta; el modelo de observación de Elle muestra por qué las dependencias ocultas no se pueden recuperar simplemente generando más historias: las escrituras ciegas en registros "destruyen la historia" (Elle §§3–4.3). Lea ejemplos de contratos para ver límites trabajados.
En JavaScript, un código de salida del proceso, el estado del ejecutor de pruebas o una consola limpia son tales observaciones: su significado depende del modo efectivo, los listeners instalados, la configuración del ejecutor y la compilación. Con un manejador uncaughtException instalado, el proceso de Node "saldrá con 0" a menos que el manejador establezca process.exitCode (Node process, uncaughtException). Lea canales de observación en JavaScript para los canales de Node, ejecutor de pruebas, React y Playwright.
Mantenga la observación independiente del comportamiento sospechoso
Trace cómo se obtiene el valor esperado o el invariante. Identifique código compartido y suposiciones que podrían hacer que el objetivo y el verificador coincidan en la misma respuesta incorrecta. Prefiera un modelo abstracto justificado, un invariante especificado de forma independiente o una relación válida en lugar de un algoritmo de producción copiado. Una segunda implementación es una opción: el SQL Logic Test de SQLite ejecuta sentencias contra varios motores y verifica "que todos obtengan las mismas respuestas". Una relación dentro del mismo motor es otra: SQLite vuelve a ejecutar suites con optimizaciones deshabilitadas, y NoREC de SQLancer compara una consulta optimizada con una no optimizada (Pruebas SQLite §2, §9, implementación de NoREC).
Mida la información realmente comparada. Conteos de filas iguales no establecen identidad de filas; un integrity_check saludable no establece integridad referencial, porque "no encuentra errores FOREIGN KEY". Conserve las comprobaciones parciales válidas y agregue una observación complementaria solo cuando la garantía del objetivo lo requiera (implementación de NoREC, comprobaciones de integridad SQLite). Lea observaciones parciales al elegir una referencia, normalización o testigo.
Verifique los errores permitidos y sus efectos
Derive el post-estado permitido por separado del estado devuelto. ABORT y FAIL en SQLite devuelven ambos un error de restricción, pero ABORT deshace la sentencia fallida mientras que FAIL "no deshace los cambios anteriores de la sentencia SQL que falló". Una aserción solo de error puede pasar por alto un efecto incorrecto; una aserción de reversión general puede rechazar un comportamiento legal (políticas de conflicto en SQLite).
Seleccione un observador para la promesa real, con precondiciones válidas. Para comprobaciones referenciales en SQLite, use la observación aplicable de clave foránea, la configuración de aplicación efectiva y la semántica NULL legal; no sustituya un resultado de integridad genérico (claves foráneas SQLite, foreign_key_check). Estos son contratos trabajados, no valores predeterminados para APIs arbitrarias.
Preserve el resultado y los límites de la comprobación
Distinga las propiedades evaluadas de las entradas rechazadas, errores esperados, comprobaciones omitidas y observaciones insuficientes cada vez que esa diferencia afecte la conclusión. NoREC omite una comparación cuando cualquiera de los conteos es su valor centinela -1 (por ejemplo, después de un error de consulta esperado) en lugar de contarlo como igualdad, e informa un error inesperado como un fallo. La completitud de Elle depende de la información registrada, y "las observaciones rara vez son completas" (implementación de NoREC, Elle §4.3).
Use harness-sensitivity para establecer que la observación alcanza y rechaza una violación representativa justificada de forma independiente. Conserve el testigo sin procesar para evidence-based-triage: la propia documentación de Elle recomienda "verificar las anomalías reportadas a mano" en lugar de tratar la etiqueta como autoridad final (README de Elle). La asignación general de búsqueda pertenece a bugfinding-campaign.
Dirija el razonamiento especializado elegido a semantic-differential-testing, metamorphic-testing, linearizability-checking, transactional-history-testing, numerical-oracles, resource-complexity-testing o liveness-testing; este skill posee la decisión de contrato a observación. Lea errores comunes para conocer atajos engañosos.
Devuelva el oráculo utilizable
Devuelva el productor, la garantía citada, las precondiciones efectivas, la observación ejecutable y la interpretación del resultado, con una distinción trabajada permitido/prohibido. Indique qué permanece no observable y qué evidencia debe sobrevivir a la repetición. Una contradicción presenciada solo respalda la garantía y las suposiciones realmente verificadas (Elle §§4.3 y 9).