Code Contracts

Code Contracts permiten especificar el comportamiento de un algoritmo de forma explícita la adhesión a un contrato bien claramente definido. Por lo general, estos contratos son en forma de pre y post condiciones. Además, uno también puede especificar los contratos de un tipo de comportamiento en forma de un tipo invariante . Por ahora no tienes que preocuparte acerca de cómo estos contratos se pueden definir (discutiremos esto más adelante), sin embargo, es importante entender algunos de los beneficios de utilizar contratos de código, estos incluyen:

• Proporcionar una descripción del comportamiento de alto nivel de un algoritmo;
• Fuera a los programadores a ser explícitos sobre el comportamiento de sus procedimientos
• Ayudar a detectar fallos tempranos.

.

Spec #

Spec # es un Proyecto de investigación de Microsoft que extiende el lenguaje C # 2 .0  de modo que puede definir fácilmente los contratos de código. Además, Spec # también proporciona controles en tiempo de compilación para verificar ciertas reglas definidas al compilar, por ejemplo que un objeto no nulo se pasa a un algoritmo. En esta sección veremos algunas de las características que el lenguaje Spec# introduce comenzando por las precondiciones.

Pre-condiciones

Las Pre-condiciones definen las propiedades que requiere un algoritmo funcionar adecuadamente; estas propiedades están definidas por el programador del algoritmo.

Para nuestro primer ejemplo vamos a ver cómo podemos definir una restricción no nulo para un argumento de un método:

class MyType
{
// ...
void MyAlgorithm(Parametro! parametro)
{
// ...
}
}

En el código anterior simplemente se a  añadido un  “!” después del tipo de argumento para definir una restricción de no pasar parametros null, esta restricción se comprueba en tiempo de compilación por el compilador Spec#.