Una lógica de corrección e incorrección del programa

La interpretación abstracta es un método bien conocido y ampliamente utilizado para extraer invariantes de programa sobreaproximados mediante un algoritmo de análisis de programas sólido. La solidez significa que no se pierden errores en el programa y está garantizada en principio por construcción. La completitud significa que el intérprete abstracto no informa de falsas alarmas para todas las entradas posibles, pero esto es extremadamente raro porque requiere un análisis muy preciso. Introducimos una noción más débil de completitud, llamada completitud local, que requiere que no se produzcan falsas alarmas únicamente en relación con algunas entradas de programa fijas. Basado en esta idea, introducimos una lógica de programa, llamada Lógica de Completitud Local para un dominio abstracto A, para demostrar tanto la corrección como la incorrección de las especificaciones del programa. Nuestro sistema de pruebas, que está parametrizado por un dominio abstracto A, combina razonamiento de sobreaproximación y subaproximación. En un triple demostrable ⊦ A p 𝖼 q, 𝖼 es un programa, q es una subaproximación de la más fuerte postcondición de 𝖼 sobre la entrada p, de modo que sus abstracciones en A coinciden. Esto significa que q nunca es demasiado burdo; es decir, bajo algunas suposiciones suaves, la interpretación abstracta de 𝖼 no produce falsas alarmas para la entrada p si y solo si q no tiene alarmas. Por lo tanto, demostrar ⊦ A p 𝖼 q no solo asegura que todas las alarmas levantadas en q son verdaderas, sino también que si q no levanta alarmas, entonces 𝖼 es correcto. También demostramos que si A es la abstracción directa que hace equivalentes todas las propiedades del programa, entonces nuestra lógica de programa coincide con la lógica de incorrección de O’Hearn, mientras que para cualquier otra abstracción, contrariamente al caso de la lógica de incorrección, nuestra lógica también puede establecer la corrección del programa.