Diseño por contrato

El diseño por contrato ( DbC ), también conocido como programación por contrato , programación por contrato y programación de diseño por contrato , es un enfoque para diseñar software .

Prescribe que los diseñadores de software deben definir especificaciones de interfaz formales , precisas y verificables para los componentes de software , que amplíen la definición ordinaria de tipos de datos abstractos con precondiciones , poscondiciones e invariantes . Estas especificaciones se denominan "contratos", de acuerdo con una metáfora conceptual con las condiciones y obligaciones de los contratos comerciales.

El enfoque DbC supone que todos los componentes del cliente que invocan una operación en un componente del servidor cumplirán las condiciones previas especificadas como necesarias para esa operación.

Cuando esta suposición se considera demasiado arriesgada (como en la computación multicanal o distribuida ), se adopta el enfoque inverso , lo que significa que el componente del servidor prueba que todas las condiciones previas relevantes sean verdaderas (antes o mientras se procesa la solicitud del componente del cliente ) y responde con un mensaje de error adecuado si no es así.

El término fue acuñado por Bertrand Meyer en relación con su diseño del lenguaje de programación Eiffel y descrito por primera vez en varios artículos a partir de 1986 ^{[1] [2] [3]} y las dos ediciones sucesivas (1988, 1997) de su libro Object-Oriented Software Construction . Eiffel Software solicitó el registro de marca para Design by Contract en diciembre de 2003, y le fue concedido en diciembre de 2004. ^{[4] [5]} El propietario actual de esta marca es Eiffel Software. ^{[6] [7]}

El diseño por contrato tiene sus raíces en el trabajo sobre verificación formal , especificación formal y lógica de Hoare . Las contribuciones originales incluyen:

• Una metáfora clara para guiar el proceso de diseño
• La aplicación a la herencia , en particular un formalismo para la redefinición y la vinculación dinámica
• La aplicación al manejo de excepciones
• La conexión con la documentación automática del software

La idea central de DbC es una metáfora sobre cómo los elementos de un sistema de software colaboran entre sí sobre la base de obligaciones y beneficios mutuos . La metáfora proviene de la vida empresarial, donde un "cliente" y un "proveedor" acuerdan un "contrato" que define, por ejemplo, que:

• El proveedor debe proporcionar un determinado producto (obligación) y tiene derecho a esperar que el cliente haya pagado su tarifa (beneficio).
• El cliente debe pagar la tarifa (obligación) y tiene derecho a obtener el producto (beneficio).
• Ambas partes deben cumplir ciertas obligaciones, como leyes y regulaciones, que se aplican a todos los contratos.

De manera similar, si el método de una clase en programación orientada a objetos proporciona una determinada funcionalidad, puede:

• Se espera que una determinada condición esté garantizada al ingresar a cualquier módulo cliente que lo llame: la condición previa del método , una obligación para el cliente y un beneficio para el proveedor (el método en sí), ya que lo libera de tener que manejar casos fuera de la condición previa.
• Garantizar una determinada propiedad a la salida: la postcondición del método : una obligación para el proveedor y, obviamente, un beneficio (el principal beneficio de llamar al método) para el cliente.
• Mantener una cierta propiedad, asumida a la entrada y garantizada a la salida: la clase invariante .

El contrato equivale semánticamente a un triple de Hoare que formaliza las obligaciones. Esto se puede resumir en las "tres preguntas" que el diseñador debe responder repetidamente en el contrato:

• ¿Qué espera del contrato?
• ¿Qué garantiza el contrato?
• ¿Qué mantiene el contrato?

Muchos lenguajes de programación tienen facilidades para hacer afirmaciones como estas. Sin embargo, DbC considera que estos contratos son tan cruciales para la corrección del software que deberían ser parte del proceso de diseño. De hecho, DbC aboga por escribir las afirmaciones primero . ^{[ cita requerida ]} Los contratos pueden escribirse mediante comentarios de código , implementarse mediante un conjunto de pruebas o ambos, incluso si no existe un soporte de lenguaje especial para contratos.

La noción de contrato se extiende hasta el nivel de método/procedimiento; el contrato para cada método normalmente contendrá la siguiente información: ^{[ cita requerida ]}

• Valores o tipos de entrada aceptables e inaceptables y sus significados
• Valores o tipos de retorno y sus significados
• Valores o tipos de condiciones de error y excepción que pueden ocurrir y sus significados
• Efectos secundarios
• Condiciones previas
• Condiciones posteriores
• Invariantes
• (más raramente) Garantías de rendimiento, por ejemplo, por tiempo o espacio utilizado.

Las subclases de una jerarquía de herencia pueden debilitar las precondiciones (pero no fortalecerlas) y fortalecer las poscondiciones y los invariantes (pero no debilitarlos). Estas reglas se aproximan a la subtipificación conductual .

Todas las relaciones de clase se dan entre clases de cliente y clases de proveedor. Una clase de cliente está obligada a realizar llamadas a las características del proveedor en las que el estado resultante del proveedor no sea violado por la llamada del cliente. Posteriormente, el proveedor está obligado a proporcionar un estado de retorno y datos que no violen los requisitos de estado del cliente.

Por ejemplo, un búfer de datos de un proveedor puede exigir que los datos estén presentes en el búfer cuando se llama a una función de eliminación. Posteriormente, el proveedor garantiza al cliente que cuando una función de eliminación finaliza su trabajo, el elemento de datos se eliminará, de hecho, del búfer. Otros contratos de diseño son conceptos de invariante de clase . El invariante de clase garantiza (para la clase local) que el estado de la clase se mantendrá dentro de las tolerancias especificadas al final de cada ejecución de función.

Al utilizar contratos, un proveedor no debe intentar verificar que se cumplan las condiciones del contrato (una práctica conocida como programación ofensiva) ; la idea general es que el código debe "fallar estrepitosamente" y que la verificación del contrato es la red de seguridad.

La propiedad "fail hard" de DbC simplifica la depuración del comportamiento del contrato, ya que el comportamiento previsto de cada método está claramente especificado.

Este enfoque difiere sustancialmente del de la programación defensiva , en el que el proveedor es responsable de determinar qué hacer cuando se rompe una condición previa. En la mayoría de los casos, el proveedor lanza una excepción para informar al cliente de que se ha roto la condición previa y, en ambos casos (tanto en DbC como en la programación defensiva), el cliente debe determinar cómo responder a eso. En tales casos, DbC facilita el trabajo del proveedor.

El diseño por contrato también define criterios de corrección para un módulo de software:

• Si la invariante de clase Y la precondición son verdaderas antes de que un cliente llame a un proveedor, entonces la invariante Y la poscondición serán verdaderas después de que se haya completado el servicio.
• Al realizar llamadas a un proveedor, un módulo de software no debe violar las condiciones previas del proveedor.

El diseño por contrato también puede facilitar la reutilización del código, ya que el contrato para cada fragmento de código está completamente documentado. Los contratos para un módulo pueden considerarse como una forma de documentación del software sobre el comportamiento de ese módulo.

Las condiciones del contrato nunca deben violarse durante la ejecución de un programa libre de errores. Por lo tanto, los contratos normalmente solo se verifican en modo de depuración durante el desarrollo del software. Más adelante, en el lanzamiento, las verificaciones del contrato se desactivan para maximizar el rendimiento.

En muchos lenguajes de programación, los contratos se implementan con assert . Las aserciones se compilan de forma predeterminada en modo de lanzamiento en C/C++ y se desactivan de manera similar en C# ^[8] y Java.

Al iniciar el intérprete de Python con "-O" (para "optimizar") como argumento, también provocará que el generador de código Python no emita ningún código de bytes para las afirmaciones. ^[9]

Esto elimina efectivamente los costos de tiempo de ejecución de las afirmaciones en el código de producción, independientemente de la cantidad y el gasto computacional de las afirmaciones utilizadas en el desarrollo, ya que el compilador no incluirá dichas instrucciones en la producción.

El diseño por contrato no reemplaza las estrategias de prueba habituales, como las pruebas unitarias , las pruebas de integración y las pruebas de sistema . Más bien, complementa las pruebas externas con pruebas internas propias que se pueden activar tanto para pruebas aisladas como en el código de producción durante una fase de prueba.

La ventaja de las pruebas internas es que pueden detectar errores antes de que se manifiesten como resultados no válidos observados por el cliente, lo que permite una detección más temprana y más específica de los errores.

El uso de afirmaciones puede considerarse una forma de oráculo de prueba , una forma de probar el diseño mediante la implementación del contrato.

Los lenguajes que implementan la mayoría de las características de DbC de forma nativa incluyen:

• Año 2012
• Hola
• Clojure
• Cobra
• D ^[10]
• Dafny
• Torre Eiffel
• Fortaleza
• Kotlin
• Mercurio
• Oxygene (anteriormente Chrome y Delphi Prism ^[11] )
• Racket (incluidos los contratos de orden superior, y enfatizando que las violaciones de contratos deben culpar a la parte culpable y deben hacerlo con una explicación precisa ^[12] )
• Cuarzo
• Escala ^{[13] [14]}
• SPARK (a través del análisis estático de programas Ada )
• Vala
• VDM

Además, la combinación de métodos estándar en el Sistema de Objetos Common Lisp tiene los calificadores de método :before, :aftery :aroundque permiten escribir contratos como métodos auxiliares, entre otros usos.

Se han desarrollado varias bibliotecas, preprocesadores y otras herramientas para lenguajes de programación existentes sin soporte nativo de diseño por contrato:

• Ada , a través de pragmas GNAT para precondiciones y poscondiciones.
• do
  • DBC para preprocesador C
  • Ñu Nana
  • Herramientas de verificación formal de eCv
• C++ :
  • Impulso.Contrato
  • Herramientas de verificación formal de eCv++
  • Compilador C++ de Digital Mars a través de la extensión CTESK de C
  • La biblioteca Loki proporciona un mecanismo llamado ContractChecker que verifica que una clase siga el diseño por contrato.
  • DBC C++ Diseño por contrato para C++
• C# (y otros lenguajes .NET), a través de Code Contracts ^[15] (un proyecto de Microsoft Research integrado en .NET Framework 4.0)
• Groovy a través de GContracts
• Vaya a través de dbc o gocontracts
• Java :
  • Activo:
    • OVal con AspectJ
    • Contratos para Java (Cofoja)
    • Lenguaje de modelado Java (JML)
    • Validación de Bean (solo condiciones previas y posteriores) ^[16]
    • valid4j
    • SafeR (con referencias seguras)
  • Inactivo/desconocido:
    • Jtest (activo pero parece que DbC ya no es compatible) ^[17]
    • iContract2/JContracts
    • Contrato4J
    • jContratista
    • C4J
    • Análisis de Google CodePro
    • Contratos de Spring para el marco Spring
    • Jass Archivado el 3 de abril de 2003 en Wayback Machine.
    • Jass moderno (su sucesor es Cofoja) ^{[18] [19]}
    • JavaDbC con AspectJ
    • JavaTESK utiliza la extensión de Java
    • chex4j usando javassist
    • Java-on-contracts altamente personalizable
• JavaScript , a través de decorator-contracts, AspectJS (específicamente, AJS_Validator), Cerny.js, ecmaDebug, jsContract, dbc-code-contracts o jscategory.
• Common Lisp , a través de la función de macro o el protocolo de metaobjetos CLOS .
• Nemerle , a través de macros.
• Nim , a través de macros.
• Perl , a través de los módulos CPAN Class::Contract (por Damian Conway ) o Carp::Datum (por Raphael Manfredi).
• PHP , a través de PhpDeal, Praspel o ContractLib de Stuart Herbert.
• Python , que utiliza paquetes como deal, icontract, PyContracts, dpcontracts o zope.interface. En PEP-316 de 2003 se propuso un cambio permanente en Python para admitir el diseño por contratos, pero se pospuso.
• Ruby , a través de DesignByContract de Brian McCallister, Ruby DBC ruby-contract o contract.ruby.
• Óxido a través de la caja de contratos.
• Vuelo veloz a través del cocoapod, por Jim Boyd.
• Tcl , a través de la extensión orientada a objetos XOTcl .

• Ingeniería de software basada en componentes
• Corrección (informática)
• Programación defensiva
• Sistema de fallo rápido
• Métodos formales
• Lógica antigua
• Programación modular
• Derivación de programas
• Refinamiento del programa
• Tipificación fuerte
• Desarrollo basado en pruebas
• Análisis de tipo de estado

• El poder del diseño por contrato(TM) Una descripción de alto nivel de DbC, con enlaces a recursos adicionales.
• Creación de software OO sin errores: una introducción al diseño por contrato (TM) Material antiguo en DbC.
• Ventajas y desventajas; implementación en RPS-Obix
• Uso de contratos de código para un código más seguro