Síntesis y equivalencia
Proteja la estructura de cálculos importantes verificando que conservan sus resultados.
Reconstruya el propio cálculo#
La síntesis inductiva guiada por contraejemplos, CEGIS, busca un cálculo alternativo a partir del comportamiento y de contraejemplos. En regiones escalares puras compatibles, construye candidatos con otra base booleana-aritmética y estructura de evaluación. Puede cambiar el propio grafo de expresiones, no solo adornar sus instrucciones.
Un contraejemplo orienta al siguiente candidato#
El candidato se somete a validación regional. Si una entrada demuestra una divergencia, ese testigo vuelve a la síntesis y el siguiente candidato debe tenerlo en cuenta. Se establece un ciclo explícito de búsqueda y prueba, en lugar de aceptar una fórmula por superar unos pocos ejemplos.
Solo se acepta una reescritura regional demostrada#
El validador distingue PROVED, COUNTEREXAMPLE_FOUND, OUT_OF_SCOPE y UNKNOWN_BUDGET_EXCEEDED. Solo PROVED permite aceptar. Agotar el presupuesto no equivale a éxito; una región fuera del modelo admitido no puede reutilizar una prueba de otro ámbito.
Explore las reglas de decisión. Este diagrama no ejecuta un solver.
R₀(x)R₁(x)Resultados + traps + precondiciones
Se acepta el candidato dentro del modelo y precondiciones declarados. El veredicto afecta a esa reescritura, no a toda la aplicación.
Una entrada concreta revela una diferencia. Se rechaza el candidato y el testigo vuelve a la síntesis.
La región incumple obligaciones de pureza, propiedad, frame o límites. No puede aceptarse bajo este modelo.
El presupuesto se agota sin prueba. El resultado inconcluso no autoriza la reescritura ni se almacena como prueba exitosa.
La prueba tiene un contrato preciso#
El modelo compara resultados exactos de 32/64 bits y comportamiento de traps bajo las precondiciones y obligaciones de frame declaradas. Incluye anchos con signo, desbordamiento y división por cero. Las regresiones cubren precondiciones ausentes, traps distintos, resultados inconclusos y caché de pruebas.
Es una propiedad de corrección limitada a la región aceptada, no una prueba de que toda la aplicación esté libre de errores o sea imposible de analizar. La validación de la aplicación y el modelo de seguridad siguen siendo responsabilidades separadas.