Relación entre contratos y mecanografía dependiente
31
He estado leyendo algunos artículos sobre tipos dependientes y contratos de programación. De la mayoría de lo que he leído, parece que los contratos se comprueban dinámicamente y los tipos dependientes se comprueban estáticamente.
Ha habido algunos documentos que me han hecho pensar que es posible tener contratos que están parcialmente controlados estáticamente:
Con esto, parece haber una gran cantidad de superposición y mi categorización de contratos frente a tipos dependientes comienza a desaparecer.
¿Hay algo más profundo en cualquiera de los conceptos que me falta? ¿O son estas realmente categorías difusas de representar el mismo concepto subyacente?
En un nivel práctico, los contratos son afirmaciones. Le permiten verificar las propiedades (sin cuantificador) de las ejecuciones individuales de un programa. La idea clave en el corazón de la verificación de contratos es la idea de la culpa, básicamente, usted quiere saber quién tiene la culpa de una violación del contrato. Esto puede ser una implementación (que no calcula el valor prometido) o la persona que llama (que pasó una función del tipo de valor incorrecto).
La idea clave es que puede rastrear la culpa utilizando la misma maquinaria que los pares de incrustación-proyección en la construcción del límite inverso de la teoría de dominios. Básicamente, cambia de trabajar con aserciones a trabajar con pares de aserciones, una de las cuales culpa al contexto del programa y la otra culpa al programa. Luego, esto le permite ajustar funciones de orden superior con contratos, porque puede modelar la contravarianza del espacio de funciones intercambiando el par de aserciones. (Ver el artículo de Nick Benton "Deshacer escritura dinámica" , por ejemplo).
Los tipos dependientes son tipos. Los tipos especifican reglas para afirmar si ciertos programas son aceptables o no. Como resultado, no incluyen cosas como la noción de culpa, ya que su función es evitar que existan programas de mal comportamiento en primer lugar. No hay nada que culpar ya que solo los programas bien formados son incluso expresiones gramaticales. Pragmáticamente, esto significa que es muy fácil usar tipos dependientes para hablar de propiedades de términos con cuantificadores (por ejemplo, que una función funciona para todas las entradas).
Estas dos vistas no son lo mismo, pero están relacionadas. Básicamente, el punto es que con los contratos, comenzamos con un dominio universal de valores y usamos contratos para reducir las cosas. Pero cuando usamos tipos, intentamos especificar dominios de valores más pequeños (con una propiedad deseada) por adelantado. Entonces podemos conectar los dos a través de familias de relaciones dirigidas por tipo (es decir, relaciones lógicas). Por ejemplo, vea "La culpa de todos" de Ahmed, Findler, Siek y Wadler , o "El significado de los tipos de Reynolds : de la semántica intrínseca a la semántica extrínseca" .
¿Por qué dice que los contratos son libres de cuantificadores?
Radu GRIGore
3
Debido a que generalmente no puede usar pruebas para establecer propiedades de funciones universalmente cuantificadas, eso es todo.
Neel Krishnaswami
3
A menos que los cuantificadores se extiendan sobre dominios finitos, en cuyo caso pueden verse como grandes conjunciones y disyunciones. O, si desea obtener fantasía, puede verificar ciertos tipos de declaraciones cuantificadas, siempre que los cuantificadores se extiendan sobre los tipos de búsqueda de Martin Escardo (que pueden ser infinitos).
Andrej Bauer
2
@Radu: Llamo a cosas como JML & co "lógicas de programa". Los lenguajes de afirmación de las lógicas de los programas no se limitan a ser términos del lenguaje de los programas. Esto le permite descartar cosas como afirmaciones no determinantes o de efectos secundarios, que no tienen una buena interpretación lógica. (Sin embargo, este tipo de cosas importan para la comprobación de contrato - ver trabajos recientes Pucella y de Tove en ESOP sobre el uso, contratos con estado imperativas para rastrear las propiedades de linealidad.)
El problema (bastante abstracto) que atacan tanto los tipos como los contratos es "¿Cómo asegurar que los programas tengan ciertas propiedades?". Aquí existe una tensión inherente entre poder expresar una clase más amplia de propiedades y poder verificar que un programa tenga o no una propiedad. Los sistemas de tipos generalmente aseguran una propiedad muy específica (el programa nunca se bloquea de ciertas maneras) y tienen un algoritmo de verificación de tipos. Por otro lado, los contratos le permiten especificar un rango muy amplio de propiedades (por ejemplo, la salida de este programa es un número primo) pero no vienen con un algoritmo de verificación.
Sin embargo, el hecho de que no exista un algoritmo de verificación de contratos (que siempre funciona) no significa que no haya casi algoritmos de verificación de contratos (que tienden a funcionar en la práctica). Le recomendaría que mire las especificaciones # y el plugin Jessie de Frama-C . Ambos trabajan expresando "este programa obedece este contrato" como una declaración en la lógica de primer orden a través de la generación de la condición de verificación , y luego solicitan un SMTsolucionador para ir a buscar una prueba. Si el solucionador no puede encontrar una prueba, entonces el programa está equivocado o, bueno, el solucionador no pudo encontrar una prueba que exista. (Es por eso que este es un "casi" algoritmo de verificación de contratos). También hay herramientas basadas en la ejecución simbólica, lo que significa aproximadamente que "este programa obedece este contrato" se expresa como un conjunto de proposiciones (en cierta lógica). Ver, por ejemplo, jStar .
El trabajo de Flanagan intenta tomar lo mejor de ambos mundos para que pueda verificar rápidamente las propiedades tipográficas y luego trabajar para el resto. No estoy realmente familiarizado con los tipos híbridos, pero sí recuerdo que el autor dijo que su motivación fue encontrar una solución que requiera menos anotaciones (que su trabajo anterior en ESC / Java). En cierto sentido, sin embargo, también existe cierta integración flexible entre los tipos y los contratos en ESC / Java (y en la Especificación #): cuando se verifican los contratos, se le dice al solucionador que la verificación de tipos tuvo éxito para que pueda ver esa información.
Los contratos se pueden verificar de forma estática. Si nos fijamos en el antiguo trabajo de Dana Xu en ESC / Haskell , ella pudo implementar la verificación completa del contrato en tiempo de compilación, solo confiando en un probador de teoremas para la aritmética. La terminación se resuelve con un límite de profundidad simple si no recuerdo mal:
Tanto los contratos como los tipos le permiten representar especificaciones de estilo Hoare (condición previa / posterior) en las funciones. Ambos pueden verificarse estáticamente en tiempo de compilación o dinámicamente en tiempo de ejecución.
Los tipos dependientes le permiten codificar una amplia gama de propiedades en el sistema de tipos, los tipos de propiedades que los programadores por contrato esperan. Esto se debe a que pueden depender de los valores del tipo. Los tipos dependientes tienden a verificarse estáticamente, aunque creo que los documentos que citó analizan enfoques alternativos.
En definitiva, hay poca diferencia. Creo que es más que los tipos dependientes son una lógica en la que puedes expresar especificaciones, mientras que los contratos son una metodología de programación en la que expresas especificaciones.
Es un poco engañoso decir que las anotaciones de estilo Hoare se pueden verificar de forma estática. Si la lógica es FO, como suele ser, entonces el problema es ciertamente indecidible. Pero sí, sé que querías decir que uno puede intentar e incluso tener éxito en muchas situaciones.
Radu GRIGore
1
Tenía la impresión de que generar la prueba puede ser indecidible, pero verificar una prueba debería serlo. Muchos lenguajes de tipo dependiente confían en que el usuario proporcione el valor de prueba de la habitación del tipo de teorema.
Jason Reich
Tienes razón. Pero vivo en el mundo automatizado, donde al usuario generalmente no se le pide una prueba.
El problema (bastante abstracto) que atacan tanto los tipos como los contratos es "¿Cómo asegurar que los programas tengan ciertas propiedades?". Aquí existe una tensión inherente entre poder expresar una clase más amplia de propiedades y poder verificar que un programa tenga o no una propiedad. Los sistemas de tipos generalmente aseguran una propiedad muy específica (el programa nunca se bloquea de ciertas maneras) y tienen un algoritmo de verificación de tipos. Por otro lado, los contratos le permiten especificar un rango muy amplio de propiedades (por ejemplo, la salida de este programa es un número primo) pero no vienen con un algoritmo de verificación.
Sin embargo, el hecho de que no exista un algoritmo de verificación de contratos (que siempre funciona) no significa que no haya casi algoritmos de verificación de contratos (que tienden a funcionar en la práctica). Le recomendaría que mire las especificaciones # y el plugin Jessie de Frama-C . Ambos trabajan expresando "este programa obedece este contrato" como una declaración en la lógica de primer orden a través de la generación de la condición de verificación , y luego solicitan un SMTsolucionador para ir a buscar una prueba. Si el solucionador no puede encontrar una prueba, entonces el programa está equivocado o, bueno, el solucionador no pudo encontrar una prueba que exista. (Es por eso que este es un "casi" algoritmo de verificación de contratos). También hay herramientas basadas en la ejecución simbólica, lo que significa aproximadamente que "este programa obedece este contrato" se expresa como un conjunto de proposiciones (en cierta lógica). Ver, por ejemplo, jStar .
El trabajo de Flanagan intenta tomar lo mejor de ambos mundos para que pueda verificar rápidamente las propiedades tipográficas y luego trabajar para el resto. No estoy realmente familiarizado con los tipos híbridos, pero sí recuerdo que el autor dijo que su motivación fue encontrar una solución que requiera menos anotaciones (que su trabajo anterior en ESC / Java). En cierto sentido, sin embargo, también existe cierta integración flexible entre los tipos y los contratos en ESC / Java (y en la Especificación #): cuando se verifican los contratos, se le dice al solucionador que la verificación de tipos tuvo éxito para que pueda ver esa información.
fuente
Los contratos se pueden verificar de forma estática. Si nos fijamos en el antiguo trabajo de Dana Xu en ESC / Haskell , ella pudo implementar la verificación completa del contrato en tiempo de compilación, solo confiando en un probador de teoremas para la aritmética. La terminación se resuelve con un límite de profundidad simple si no recuerdo mal:
fuente
Tanto los contratos como los tipos le permiten representar especificaciones de estilo Hoare (condición previa / posterior) en las funciones. Ambos pueden verificarse estáticamente en tiempo de compilación o dinámicamente en tiempo de ejecución.
Los tipos dependientes le permiten codificar una amplia gama de propiedades en el sistema de tipos, los tipos de propiedades que los programadores por contrato esperan. Esto se debe a que pueden depender de los valores del tipo. Los tipos dependientes tienden a verificarse estáticamente, aunque creo que los documentos que citó analizan enfoques alternativos.
En definitiva, hay poca diferencia. Creo que es más que los tipos dependientes son una lógica en la que puedes expresar especificaciones, mientras que los contratos son una metodología de programación en la que expresas especificaciones.
fuente