Diseño por contratos: construyendo software confiable

En (Mitchel, 2002) R.Mitchell y J.McLim se enumeran una serie de principios a seguir cuando se diseñan clases utilizando contratos de software. Ellos realizan una extensa discusión y ejemplificación de dichos principios. En este artículo se enumeran los mismos:

Principio 1: Separar consultas de comandos . Este principio también es explicado detalladamente en (Meyer,1997). La idea es que las rutinas de una clase deben ser (en lo posible) o comandos o consultas pero no ambas cosas. Las consultas devuelven un valor (ej. funciones) y los comandos pueden cambiar el estado interno del objeto.
Principio 2: Separar consultas básicas de consultas derivadas. La intención es conseguir un conjunto de especificación formado por consultas que denominamos básicas, de tal forma que el resto de las consultas puedan derivarse de las básicas.
Principio 3: Para cada consulta derivada escribir una poscondición especificando su resultado en términos de una o más consultas básicas. Esto permite conocer el valor de las consultas derivadas conociendo el valor de las consultas básicas. Idealmente, sólo el conjunto minimal de especificación tiene la obligación de ser exportado públicamente.
Principio 4: Para cada comando escribir una precondición que especifique el valor de cada consulta básica. Dado que el resultado de todas las consultas puede visualizarse a través de las consultas básicas, con este principio se garantiza el total conocimiento de los efectos visibles de cada comando.
Principio 5: Para toda consulta o comando decidir una precondición adecuada. Este principio se auto explica ya que permite definir claramente el contrato de cada rutina.
Principio 6: Escribir el invariante para definir propiedades de los objetos. La idea aquí es ayudar al lector a construir un modelo conceptual apropiado de la clase.

Junto a estos principios los autores también explican una serie de guías y clases auxiliares para escribir contratos. Los principios enumerados junto al estudio de bibliotecas de clases (ej. EiffelBase) son una importante fuente de aprendizaje para el diseño de contratos.

Si bien el lenguaje Eiffel tiene soporte nativo para diseño por contratos y el mismo es parte integrante de la cultura asociada al lenguaje, existen implementaciones para el soporte por contratos en otros lenguajes. Una de las más notorias es la implementación de contratos para el lenguaje JAVA llamada iContract (Kramer,1998). Básicamente iContract es un pre-procesador de código fuente que permite instrumentar invariantes de clase, pre y poscondiciones que pueden asociarse a métodos e interfaces en JAVA. Para lograrlo, utilizan marcas de comentario especiales como @pre y @post que al ser interpretadas por iContract se convierten en código para el chequeo de aserciones que se insertan en el código fuente. Las expresiones permitidas son un subconjunto del OCL (Object Constraint Language) de UML. Entre las características notables se incluye el soporte para cuantificadores (forall y exists). Cuenta además con soporte para la propagación de invariantes, pre y poscondiciones por medio de la herencia y la implementación de múltiples interfaces. Dado que los comentarios no son obligatorios, el código fuente que contenga anotaciones de diseño por contratos puede ser a su vez procesado por cualquier compilador Java que ignorará los mismos.

Entre las ventajas de iContract está el hecho de estar libremente disponible. Puede ser descargado desde http://www.reliable-systems.com/ contando además con soporte para VisualAge for Java. El siguiente fragmento de código muestra el uso de iContract:

Hay otras implementaciones disponibles para JAVA. Entre ellas una denominada Jass, por Java with assertions, que también está basada en un pre-procesador. El siguiente código muestra un ejemplo:

Hay una implementación de contratos de software realizada para los lenguajes C# y VB.NET en el marco de Microsoft .NET, llamada el Design by Contract Framework. Básicamente se trata de una librería que provee un conjunto de métodos estáticos para definir precondiciones, poscondiciones e invariantes de clase junto a aserciones más generales. Se creó para ello un espacio de nombres (namespace) denominado DesignByContract. La sintaxis para las aserciones en C# es la siguiente:

Check.Require( [expresión boolena] ); //precondición

Check.Ensure( [expresión boolena] ); //poscondición

Check.Invariant( [expresión boolena] ); // Invariante de clase

Esta implementación, que fue creada por Kevin McFarlane, también está libremente disponible en: http://www.codeproject.com/csharp/designbycontract.asp. Existen, además, implementaciones de diseño por contratos para C++, LISP y otros lenguajes (Plosch,1999) (Hunt,2000).