DevLabs: Code Contracts para .NET
Publicación del inglés original: Lunes, 23 de febrero de 2009 14:11 PST por Somasegar
En octubre del año pasado, hablé de DevLabs (en inglés): un sitio dedicado a las innovaciones de software para la comunidad de desarrolladores.
Hoy, DevLabs ha publicado una innovación en la que nuestro grupo de investigación Microsoft Research ha estado trabajando: Code Contracts para .NET (en inglés).
El diseño por contrato (Design-by-contract) es una idea pionera de Eiffel. El lanzamiento de hoy, Code Contracts para. NET, es un mecanismo general de diseño por contrato que ahora todos los programadores de .NET pueden utilizar. Mediante su utilización, los programadores proporcionan precondiciones y postcondiciones de método que amplían las API existentes con información que no se puede expresar en los sistemas de tipo de lenguajes de .NET. Además, los contratos especifican las invariantes de objeto, que definen qué estados permitidos puede tener una instancia de una clase (es decir su coherencia interna).
Los contratos se utilizan para comprobaciones en tiempo de ejecución, verificación estática y generación de documentación. Los contratos también permiten documentación automática y pruebas mejoradas. Code Contracts para .NET está formado por tres componentes: los métodos de biblioteca estáticos utilizados para expresar los contratos, un reescritor binario y un corrector estático.
Los métodos de biblioteca (Library Methods)
El método estático Contract.Requires() se utiliza para precondiciones y Contract.Ensures() se utiliza para postcondiciones. Los programadores escriben las llamadas a estos métodos como un preámbulo al principio de un método. El método de Contract.Invariant() sirve para especificar las invariantes de objeto. Todos las invariantes de objeto se colocan en un método marcado con el atributo [ContractInvariantMethod].
Puede ver cómo se utilizan en la pantalla siguiente. Observe el uso del método Contract.OldValue() dentro de la postcondición que remite a los valores existentes al principio del método. El código se compila mediante el compilador .NET normal, por ejemplo, C#, para generar el lenguaje intermedio.
El reescritor binario (Binary Rewriter)
El lenguaje intermedio que genera el compilador de C# para el ejemplo anterior no se puede ejecutar tal y como está. Para proporcionar la comprobación de los contratos en tiempo de ejecución, el reescritor binario toma el lenguaje intermedio compilado y lo transforma para que los contratos se evalúen en puntos del programa correcto. Por ejemplo, las postcondiciones se evalúan justo antes de cada punto de retorno dentro de un método. Cualquier expresión dentro de una llamada a OldValue() se evalúa en la entrada al método con el valor correspondiente y reemplaza la llamada cuando la postcondición se evalúa. (También existe el método Result() que se utiliza para hacer referencia al valor devuelto de un método. Su uso se ilustra a continuación). Si el código instrumentado sigue una ruta de ejecución que infringe un contrato, hay un componente de notificación programable que indica que existe un error. Puede ver un ejemplo en la captura de pantalla siguiente, que muestra una precondición con errores en tiempo de ejecución: el método Divide esperaba un argumento distinto de cero. (En este ejemplo, la notificación dio como resultado un cuadro de diálogo de aserción, pero se puede personalizar para realizar cualquier acción que se desee.)
El Comprobador estático (Static Checker)
Esta herramienta analiza el código para buscar las infracciones de contrato sin tener que ejecutar el código. El correcto genera advertencias si no es capaz de determinar que el código es correcto para todas las ejecuciones posibles.
En el ejemplo de la siguiente captura de pantalla el corrector advierte de una posible precondición errónea en la llamada de MyMath.GCD.
Si el programador agrega la precondición a NormalizedRational que x debe ser no negativo e y debe ser positivo, el corrector demuestra que se satisface la precondición de MyMath.GCD en todas las ejecuciones posibles.
Además, el corrector demuestra que MyMath.GCD siempre satisface su postcondición (es decir, GCD es positivo). El corrector utiliza la postcondición de GCD para demostrar: que en línea 45 nunca hay una división entre cero y que "y/gcd" es distinto de cero, para que se cumpla siempre la precondición del constructor Rational.
Y, por supuesto, puede utilizar Code Contracts directamente en Visual Studio. Instalar el archivo msi de Code Contracts habilita la ficha "Code Contracts" en las propiedades del proyecto donde se pueden establecer las preferencias para la utilización de Code Contracts. Para las configuraciones en las que no se realicen comprobaciones en tiempo de ejecución, los métodos de biblioteca se compilan separadamente a través de los atributos de compilación condicionales en sus definiciones. ¡Una función muy nueva de .NET!. Así, no hay pérdida de rendimiento en el código para contratos que no desee ejecutar.
He aquí algunos comentarios de un cliente que tuvo la oportunidad de evaluar una versión preliminar. "Es un producto realmente interesante. He disfrutado de la combinación del reescritor y la biblioteca, que lo hace independiente de cualquier lenguaje. No puedo esperar para ver las herramientas mejorar."
¡Namaste!