coq - tag - body definicion

Definición de un programa certificado. (5)

Veo un par de grupos de investigación diferentes, y al menos un libro, que hablan sobre el uso de Coq para diseñar programas certificados. ¿Hay consenso sobre cuál es la definición de programa certificado ? Por lo que puedo decir, todo lo que realmente significa es que el programa se mostró total y correcto. Ahora, el tipo de programa puede ser algo realmente exótico, como una lista con una prueba de que no está vacío, ordenado, con todos los elementos> = 5, etc. Sin embargo, en última instancia, es un programa certificado que solo muestra que Coq es total y seguro. , donde todas las preguntas interesantes se reducen a lo que se incluyó en el tipo final?

Editar 1

Basándome en la respuesta de wjedynak, eché un vistazo al documento de Xavier Leroy "Verificación formal de un compilador realista", que está vinculado en las respuestas a continuación. Creo que esto contiene buena información, pero creo que la información más informativa en esta secuencia de investigación se puede encontrar en el artículo Semántica mecanizada para el subconjunto del Clight del lenguaje C por Sandrine Blazy y Xavier Leroy. Este es el lenguaje en el que el documento "Verificación formal" agrega optimizaciones. En ella, Blazy y Leroy presentan la sintaxis y la semántica del lenguaje Clight y luego discuten la validación de esta semántica en la sección 5. En la sección 5, hay una lista de diferentes estrategias utilizadas para validar el compilador, que en cierto sentido proporciona una visión general de diferentes estrategias para la creación de un programa certificado . Estos son:

Revisiones manuales
Demostrando propiedades de la semántica.
Traducciones verificadas
Pruebas semánticas ejecutables.
Equivalencia con semántica alternativa.

En cualquier caso, probablemente hay puntos que podrían agregarse y sin duda me gustaría saber más.

Volviendo a mi pregunta original acerca de cuál es la definición de un programa certificado, todavía no me queda claro. Wjedynak proporciona una respuesta, pero realmente el trabajo de Leroy involucró la creación de un compilador en Coq y luego, en cierto sentido, lo certificó. En teoría, hace posible ahora probar cosas sobre los programas de C ya que ahora podemos ir C-> Coq-> proof. En ese sentido, parece que hay un flujo de trabajo donde podríamos

Escribe un programa en lenguaje X
Forma de un modelo del programa del paso 1 en Coq o alguna otra herramienta de asistente de prueba. Esto podría implicar la creación de un modelo del lenguaje de programación en Coq o la creación de un modelo del programa directamente (es decir, volver a escribir el programa en Coq).
Probar alguna propiedad sobre el modelo. Tal vez sea una prueba sobre los valores. Tal vez sea la prueba de la equivalencia de las declaraciones (cosas como 3 = 1 + 2 o f (x, y) = f (y, x), lo que sea.)
Luego, en base a estas pruebas, llame al programa original certificado.

Alternativamente, podríamos crear una especificación de un programa en una herramienta de asistente de prueba y luego probar las propiedades de la especificación, pero no el programa en sí.

En cualquier caso, todavía estoy interesado en escuchar definiciones alternativas si alguien las tiene.

En primer lugar, tenga en cuenta que la frase "certificado" tiene un sesgo ligeramente francés: en otros lugares, la expresión "verificado" o "probado" se usa a menudo.

En cualquier caso, es importante preguntar qué significa eso en realidad. X. Leroy y CompCert es un muy buen punto de partida: es un gran proyecto sobre la verificación del compilador de C, y Leroy siempre está dispuesto a explicar a su audiencia por qué la verificación es importante. Especialmente cuando se habla con personas de "agencias de certificación" que usualmente significan pruebas, no pruebas.

Otro gran proyecto de verificación es L4.verified que usa Isabelle / HOL. Esta parte de la exposition explica un poco lo que realmente se afirma y se demuestra, y cuáles son las consecuencias. Desafortunadamente, la prueba real es de alto secreto, por lo que no puede ser verificada públicamente.

Estoy de acuerdo en que la noción parece vaga, pero a mi entender, un programa certificado es un programa equipado con la prueba de corrección. Ahora, al usar firmas de tipo rico y expresivo, puede hacerlo para que no haya necesidad de una prueba por separado, pero a menudo esto es solo una cuestión de conveniencia. El problema real es qué entendemos por corrección: es una cuestión de especificación. Puedes echar un vistazo a, por ejemplo, Xavier Leroy. Verificación formal de un compilador realista .

Puede significar que está libre de error de tiempo de ejecución (desbordamiento numérico, referencias no válidas ...), que ya es bueno en comparación con el software más desarrollado, aunque aún es débil. El otro significado se demuestra que es correcto de acuerdo con la formalización de un dominio; es decir, no solo tiene que estar formalmente libre de errores de tiempo de ejecución, sino que también se debe probar que hace lo que se espera que haga (que debe haber sido definido con precisión).

Un programa certificado es un programa que se combina con una prueba de que el programa cumple con sus especificaciones, es decir, un certificado. La clave es que existe un objeto de prueba que puede verificarse independientemente de la herramienta que produjo la prueba.

Un programa verificado ha sido verificado, lo que en este contexto normalmente puede significar que su especificación se ha formalizado y se ha demostrado que es correcta en un sistema como Coq, pero la prueba no está necesariamente certificada por una herramienta externa.

Esta distinción está bien documentada en la literatura científica y no es específica de los francófonos. Xavier Leroy lo describe muy claramente en la Sección 2.2 de Un back-end de compilador verificado formalmente .

share tengo entendido, en este sentido, "certificado" es, share , una palabra inglesa elegida por francófonos en la que los hablantes nativos podrían haber usado "verificado formalmente". Coq fue desarrollado en Francia y tiene muchos desarrolladores y usuarios de habla francesa.

En cuanto a lo que significa "verificación formal", Wikipedia notes (licencia: CC BY-SA 3.0 ) que:

es el acto de probar ... la corrección de los algoritmos previstos subyacentes a un sistema con respecto a una determinada especificación formal o propiedad, utilizando métodos formales de matemáticas.

(Me doy cuenta de que le gustaría una definición mucho más precisa que esta. Espero actualizar esta respuesta en el futuro, si la encuentro).

Wikipedia señala especialmente la diferencia entre verificación y validación :

Validación: "¿Estamos tratando de hacer lo correcto?", Es decir, ¿el producto está especificado para las necesidades reales del usuario?
Verificación: "¿Hemos hecho lo que intentábamos hacer?", Es decir, ¿el producto cumple con las especificaciones?

El documento de landmark seL4: Verificación formal de un núcleo de OS (Klein, et al., 2009) corrobora esta interpretación:

Un cínico podría decir que una prueba de implementación solo muestra que la implementación tiene exactamente los mismos errores que contiene la especificación. Esto es cierto: la prueba no garantiza que la especificación describa el comportamiento que espera el usuario. La diferencia [en un enfoque verificado comparado con uno no verificado] es el grado de abstracción y la ausencia de clases enteras de errores.

¿Qué clase de bichos son esos? El tutorial de Agda da una idea :

no hay errores de tiempo de ejecución (los errores inevitables como los errores de E / S se manejan; otros se excluyen por diseño).
No hay bucles infinitos no productivos.