haskell - que - principios de diseño de software solid
Comparando el diseño por contrato con los sistemas tipográficos. (5)
Creo que DbC y los sistemas de tipo no son comparables. Existe una confusión entre DbC y sistemas de tipo (o incluso sistemas de verificación). Por ejemplo, podemos encontrar la comparación de DbC y la herramienta Liquid Haskell o el marco de DbC y QuickCheck. En mi humilde opinión no es correcto: los sistemas de tipo, así como los sistemas de prueba formal, afirman solo uno: usted: tiene algunos algoritmos en mente y declara las propiedades de estos algoritmos. Entonces implementas estos algoritmos. Los sistemas de tipos y los sistemas de prueba formal verifican que el código de implementación corresponde a las propiedades declaradas.
DbC verifica no las cosas internas (implementación / código / algoritmo) sino las cosas externas: características esperadas de las cosas que son externas a su código. Puede ser el estado del entorno, el sistema de archivos, la base de datos, las personas que llaman, seguro su propio estado, cualquier cosa. Los contratos típicos funcionan en tiempo de ejecución, no en tiempo de compilación o en una fase de verificación especial.
Ejemplo canónico de DbC muestra cómo se encontró un error en el chip HP. Ocurre porque DbC declara las propiedades del componente externo: del chip, su estado, las transiciones, etc. Y si su aplicación llega a un estado inesperado del mundo externo, notifica tal caso como una excepción. La magia aquí es que: 1) define los contratos en un solo lugar y no se repite 2) los contratos pueden desactivarse fácilmente (eliminarse de un binario compilado). Están más cerca de los Aspectos IMHO, ya que no son "lineales" como las llamadas de subrutinas.
Mi resumen aquí es que DbC es más útil para evitar errores del mundo real que los sistemas de tipos, porque la mayoría de los errores reales ocurren debido a una mala interpretación del comportamiento de world / environment / frameworks / OS components / etc. Los tipos y la asistencia de asistencia solo ayudan a evitar sus propios errores simples que se pueden encontrar con pruebas o modelos (en MatLab, Mathematica, etc., etc.).
En resumen: no se pueden encontrar errores en el chip HP con tipos de sistema. Claro, existe la ilusión de que es posible algo así como las mónadas indexadas, pero el código real con tales intentos parecerá super complejo, insostenible y no práctico. Pero creo que son posibles algunos esquemas híbridos.
Hace poco leí un artículo que comparaba el diseño por contrato con el desarrollo guiado por pruebas. Parece que hay mucha superposición, cierta redundancia y un poco de sinergia entre el DbC y el TDD. Por ejemplo, hay sistemas para generar automáticamente pruebas basadas en contratos.
¿De qué manera se superpone DbC con el sistema de tipo moderno (como en haskell, o uno de esos lenguajes de tipo dependiente) y hay puntos en los que usar ambos es mejor que cualquiera?
El DBC es valioso siempre y cuando no pueda expresar todos los supuestos en el propio tipo systen. Ejemplo de haskell simple:
take n [] = []
take 0 _ = []
take n (a:as) = take (n-1) as
El tipo sería:
take :: Int -> [a] -> [a]
Sin embargo, solo los valores mayores-iguales a 0 están bien para n. Aquí es donde DBC podría intervenir y, por ejemplo, generar las propiedades de comprobación rápida adecuadas.
(Por supuesto, en este caso, es demasiado fácil verificar los valores negativos y corregir un resultado que no sea indefinido, pero hay casos más complejos).
El documento "Contratos mecanografiados para la programación funcional" por Ralf Hinze, Johan Jeuring y Andrés Löh tenía esta práctica tabla que ilustra los contratos de paradero ubicados en el espectro de diseño de "verificación":
| static checking | dynamic checking
-------------------------------------------------------------------
simple properties | static type checking | dynamic type checking
complex properties | theorem proving | contract checking
Mira aquí:
Las diferencias principales son que las pruebas son dinámicas e incompletas, confiando en la medición para evidenciar que usted ha validado completamente la propiedad que está probando, mientras que los tipos y la comprobación de tipos son un sistema formal que garantiza que todas las rutas de código posibles han sido validadas contra cualquier propiedad que sea. indicando en tipos.
La prueba de una propiedad solo puede aproximarse al límite del nivel de seguridad que una verificación de tipo para la misma propiedad proporciona de forma inmediata. Los contratos aumentan la línea de base para la verificación dinámica.
Parece que la mayoría de las respuestas asumen que los contratos se verifican dinámicamente . Tenga en cuenta que en algunos sistemas los contratos se verifican estáticamente . En tales sistemas, puede pensar en los contratos como una forma restringida de tipos dependientes que pueden verificarse automáticamente. Compare esto con los tipos dependientes más ricos, que se verifican interactivamente, como en Coq.
Consulte la sección "Comprobación de especificaciones" en la página de Dana Xu para obtener información sobre la verificación estática e híbrida (estática seguida de dinámica) de los contratos de Haskell y OCaml. El sistema de contratos de Xu incluye tipos de refinamiento y flechas dependientes, los cuales son tipos dependientes. Los idiomas iniciales con tipos dependientes restringidos que se verifican automáticamente incluyen el DML y el ATS de Pfenning y Xi. En DML, a diferencia del trabajo de Xu, los tipos dependientes están restringidos para que se complete la comprobación automática.