Diseño por contrato

Un diseño por contrato

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 el diseño de software.

Prescribe que los diseñadores de software deben definir especificaciones de interfaz formales, precisas y verificables para componentes de software, que amplían la definición ordinaria de tipos de datos abstractos con condiciones previas, condiciones posteriores 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 de DbC asume que todos los componentes de cliente que invocan una operación en un componente de servidor cumplirán las condiciones previas especificadas como requeridas para esa operación.

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

Historia

El término fue acuñado por Bertrand Meyer en relación con su diseño del lenguaje de programación Eiffel y se describió por primera vez en varios artículos a partir de 1986 y las dos ediciones sucesivas (1988, 1997) de su libro Construcción de software orientada a objetos . Eiffel Software solicitó el registro de marca para Diseño por contrato en diciembre de 2003 y se le concedió en diciembre de 2004. El propietario actual de esta marca es Eiffel Software.

El diseño por contrato tiene sus raíces en el trabajo de verificación formal, especificación formal y lógica 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 unión dinámica
• La aplicación a la tramitación de excepciones
• La conexión con la documentación automática del software

Descripción

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" acordar 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 cuota (beneficio).
• El cliente debe pagar la cuota (obligación) y tiene derecho a obtener el producto (beneficio).
• Ambas partes deben cumplir ciertas obligaciones, como leyes y reglamentos, que se aplican a todos los contratos.

Del mismo modo, si el método de una clase en la programación orientada a objetos proporciona una determinada funcionalidad, puede:

• Espere que una condición determinada sea garantizada en la entrada por 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 mismo), ya que le libera de tener que manejar casos fuera de la condición previa.
• Garantizar una determinada propiedad en la salida: la condición post del método: una obligación para el proveedor, y obviamente un beneficio (el principal beneficio de llamar el método) para el cliente.
• Mantener una determinada propiedad, asumida en la entrada y garantizada en la salida: la clase invariante.

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

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

Muchos lenguajes de programación tienen funciones 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. En efecto, DbC aboga por escribir primero las afirmaciones. Los contratos se pueden escribir mediante comentarios de código, se pueden aplicar mediante un conjunto de pruebas o ambos, incluso si no hay un soporte de idioma especial para los 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:

• Valores o tipos de insumos 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 en una jerarquía de herencia pueden debilitar las condiciones previas (pero no fortalecerlas) y fortalecer las condiciones posteriores y los invariantes (pero no debilitarlos). Estas reglas se aproximan a la subtipificación conductual.

Todas las relaciones de clase son entre clases de clientes y clases de proveedores. Una clase de cliente está obligada a realizar llamadas a las características del proveedor cuando la llamada del cliente no viole el estado resultante del proveedor. Posteriormente, el proveedor está obligado a proporcionar un estado de devolución y datos que no violen los requisitos de estado del cliente.

Por ejemplo, un búfer de datos de un proveedor puede requerir 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 termine su trabajo, el elemento de datos, de hecho, se eliminará del búfer. Otros contratos de diseño son conceptos de clase invariante. La clase invariante garantiza (para la clase local) que el estado de la clase se mantendrá dentro de las tolerancias especificadas al final de la ejecución de cada característica.

Al usar contratos, un proveedor no debe tratar de 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 con fuerza", siendo la verificación del contrato el red de seguridad.

DbC's "falla mucho" La propiedad 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, donde el proveedor es responsable de averiguar qué hacer cuando se rompe una condición previa. La mayoría de las veces, el proveedor lanza una excepción para informar al cliente que se ha roto la condición previa y, en ambos casos, DbC y programación defensiva por igual, el cliente debe descubrir cómo responder a eso. En tales casos, DbC facilita el trabajo del proveedor.

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

• Si la clase invariante Y la condición previa son verdaderas antes de que un proveedor sea llamado por un cliente, entonces el invariante Y la condición post será verdad después de que el servicio haya sido completado.
• Al hacer 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 de un módulo pueden considerarse como una forma de documentación de software para el comportamiento de ese módulo.

Implicaciones de rendimiento

Nunca se deben violar las condiciones del contrato durante la ejecución de un programa sin errores. Por lo tanto, los contratos generalmente solo se verifican en modo de depuración durante el desarrollo del software. Posteriormente, en el lanzamiento, las comprobaciones de contrato se desactivan para maximizar el rendimiento.

En muchos lenguajes de programación, los contratos se implementan con aserción. Las afirmaciones se compilan de forma predeterminada en el modo de publicación en C/C++ y se desactivan de forma similar en C# y Java.

Iniciando el intérprete de Python con "-O" (para "optimizar") como argumento también hará que el generador de código de Python no emita ningún código de bytes para afirmaciones.

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á tales instrucciones en la producción.

Relación con las pruebas de software

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

La ventaja de las autocomprobaciones internas es que pueden detectar errores antes de que se manifiesten como resultados no válidos observados por el cliente. Esto conduce a una detección de errores más temprana y más específica.

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

Soporte de idiomas

Idiomas con soporte nativo

Los idiomas que implementan la mayoría de las funciones de DbC de forma nativa incluyen:

• Ada 2012
• Ciao
• Clojure
• Cobra
• D
• Dafny
• Eiffel
• Fortaleza
• Kotlin
• Mercurio
• Oxygene (antes Chrome y Delphi Prism)
• Racket (incluidos los contratos de orden superior, y subrayando que las violaciones de contratos deben culpar al culpable y hacerlo con una explicación precisa)
• Sather
• Scala
• SPARK (a través del análisis estático de los programas Ada)
• Vala
• VDM

Además, la combinación de métodos estándar en Common Lisp Object System tiene los calificadores de método :before, :after y :around que permiten redacción de contratos como métodos auxiliares, entre otros usos.

Idiomas con soporte de terceros

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

• Ada, via GNAT pragmas para condiciones previas y posteriores.
• C y C++:
  • Boost.Contract
  • DBC for C preprocesador
  • GNU Nana
  • eCv y eCv++ instrumentos oficiales de verificación
  • Digital Mars C++ compilador a través de la extensión CTESK de C
  • Loki Library proporciona un mecanismo llamado ContractChecker que verifica una clase sigue el diseño por contrato.
  • DBC C++ Diseño por contrato para C++
• C# (y otros idiomas.NET), vía Contratos de código (un proyecto de Microsoft Research integrado en el. Marco NET 4.0)
• Groovy via GContracts
• Vaya por dbc o gocontracts
• Java:
  • Activo:
    • OVal con AspectJ
    • Contratos para Java (Cofoja)
    • Java Modeling Language (JML)
    • Validación de los frijoles (sólo condiciones previas y posteriores)
    • valid4j
    • SafeR (con referencias seguras)
  • Inactivo/no conocido:
    • Jtest (activo pero DbC parece no ser soportado más)
    • iContract2/JContracts
    • Contract4J
    • jContractor
    • C4J
    • Código de Google Pro Analytix
    • SpringContracts for the Spring Framework
    • Jass
    • Jass moderno (sucesor es Cofoja)
    • JavaDbC usando AspectJ
    • JavaTESK utilizando extensión de Java
    • chex4j usando javassist
    • altamente personalizable java-on-contracts
• JavaScript, via decorator-contracts, AspectJS (específicamente, AJS_Validator), Cerny.js, ecmaDebug, jsContract, dbc-code-contracts or jscategory.
• Lisp común, a través de la instalación macro o el protocolo de metaobjeto CLOS.
• Nemerle, a través de macros.
• Nim, a través de macros.
• Perl, a través de los módulos CPAN Clase: Contrato (por Damián Conway) o Carpa::Datum (por Raphael Manfredi).
• PHP, a través de PhpDeal, Praspel o Stuart Herbert's ContractLib.
• Python, usando paquetes como trato, iconotract, PyContracts, dpcontracts, o zope.interface. En 2003 se propuso un cambio permanente a Python para apoyar el diseño mediante contratos, pero se aplazará.
• Ruby, via Brian McCallister's DesignByContract, Ruby DBC ruby-contract o contracts.ruby.
• Rust via the contracts crate.
• Swift via the cocoapod by Jim Boyd.
• Tcl, a través de la extensión orientada al objeto XOTcl.