Contratos de código

Artículo
08/10/2011

Los contratos de código proporcionan una manera de especificar condiciones previas, condiciones posteriores y objetos invariables en su código. Las condiciones previas son requisitos que se deben cumplir al escribir un método o propiedad. Las condiciones posteriores describen las expectativas en el momento en el que sale el código de método o propiedad. Los objetos invariables describen el estado esperado para una clase que está en un buen estado.

Los contratos de código incluyen clases para marcar el código, un analizador estático para el análisis en tiempo de compilación y un analizador en tiempo de ejecución. En el espacio de nombres System.Diagnostics.Contracts se pueden encontrar las clases para contratos de código.

Entre las ventajas de contratos de código se incluyen las siguientes:

Pruebas mejoradas: los contratos de código proporcionan comprobación del contrato estática, comprobación en tiempo de ejecución y generación de documentación.
Herramientas de prueba automáticas: puede utilizar contratos de código para generar pruebas unitarias más significativas eliminando los argumentos de prueba sin sentido que no satisfacen las condiciones previas.
Comprobación estática: el comprobador estático puede decidir si hay alguna infracción del contrato sin ejecutar el programa. Comprueba los contratos implícitos, como desreferencias y límites de matriz NULL, y contratos explícitos.
Documentación de referencia: el generador de documentación aumenta los archivos de documentación XML existentes con información de contrato. Hay también hojas de estilos que se pueden utilizar con Sandcastle para que las páginas de documentación generadas tengan secciones de contrato.

Todos los idiomas de .NET Framework pueden sacar inmediatamente partido de los contratos; no tiene que escribir un analizador o compilador especial. Un complemento de Visual Studio permite especificar el nivel de análisis de contratos de código. Los analizadores pueden confirmar que los contratos están correctamente formados (comprobación de tipos y resolución de nombres) y pueden generar un formulario compilado de los contratos en formato de Lenguaje Intermedio de Microsoft (MSIL). Al crear contratos en Visual Studio, puede sacar partido del IntelliSense estándar proporcionado por la herramienta.

La mayoría de los métodos de la clase de contrato están compilados condicionalmente; es decir, el compilador solo emite las llamadas a estos métodos cuando define un símbolo especial, CONTRACTS FULL, utilizando la directiva #define. CONTRACTS FULL le permite escribir contratos en su código sin utilizar directivas #ifdef; puede generar diferentes compilaciones, algunas con contratos y otras sin ellos.

Para herramientas e instrucciones detalladas sobre el uso contratos de código, vea Code Contracts en el sitio web de MSDN DevLabs.

Preconditions

Puede expresar condiciones previas utilizando el método Contract.Requires. Las condiciones previas especifican el estado cuando se invoca un método. Generalmente, se utilizan para especificar valores de parámetro válidos. Todos los miembros que se mencionan en las condiciones previas deben ser por lo menos tan accesibles como el propio método; si no, es posible que no todos los llamadores de un método puedan entender la condición previa. La condición no debe tener ningún efecto secundario. El analizador en tiempo de ejecución determina el comportamiento en tiempo de ejecución de las condiciones previas que han generado un error.

Por ejemplo, la siguiente condición previa expresa que el parámetro x debe ser no NULL.

Contract.Requires( x != null );

Si el código debe provocar una excepción determinada al producirse un error de una condición previa, puede utilizar la sobrecarga genérica de Requires del modo siguiente.

Contract.Requires<ArgumentNullException>( x != null, "x" );

Instrucciones Requires heredada

La mayoría del código contiene alguna validación de parámetros en forma de código if-then-throw. Las herramientas de contrato reconocen estas instrucciones como condiciones previas en los siguientes casos:

Las instrucciones aparecen antes de cualquier otra instrucción en un método.
A un conjunto completo de estas instrucciones le sigue una llamada al método Contract explícita, como una llamada al método Requires, Ensures, EndContractBlock o EnsuresOnThrow.

Cuando aparecen instrucciones if-then-throw en este formulario, las herramientas las reconocen como instrucciones requires heredadas. Si ningún otro contrato sigue a la secuencia if-then-throw, finalice el código con el método Contract.EndContractBlock.

if ( x == null ) throw new ...
Contract.EndContractBlock(); // All previous "if" checks are preconditions

Observe que la condición en la prueba anterior es una condición previa negada. (La condición previa real sería x != null.) Una condición previa negada está altamente restringida: se debe escribir como se muestra en el ejemplo anterior; es decir, no debe contener ninguna cláusula else y el cuerpo de la cláusula then debe ser una instrucción throw única. La prueba if está sujeta a reglas de pureza y de visibilidad (vea Instrucciones de uso), pero la expresión throw solo está sujeta a reglas de pureza. Sin embargo, el tipo de la excepción producido debe ser tan visible como el método en el que se produce el contrato.

Postconditions

Las condiciones posteriores son contratos para el estado de un método cuando finaliza. La condición posterior se comprueba justo antes de salir de un método. El analizador en tiempo de ejecución determina el comportamiento en tiempo de ejecución de las condiciones posteriores que han generado un error.

A diferencia de las condiciones previas, las condiciones posteriores pueden hacer referencia a miembros con menos visibilidad. Un cliente quizá no puede entender o utilizar parte de la información expresada por una condición posterior mediante el estado privado, pero esto no afecta a la capacidad del cliente de utilizar el método correctamente.

Condiciones posteriores estándar

Puede expresar condiciones posteriores estándar mediante el método Ensures. Las condiciones posteriores expresan una condición que debe ser true tras una finalización normal del método.

Contract.Ensures( this .F > 0 );

Condiciones posteriores excepcionales

Unas condiciones posteriores excepcionales son condiciones posteriores que deberían ser true cuando un método provoca una excepción determinada. Puede especificar estas condiciones posteriores mediante el método Contract.EnsuresOnThrow, como se muestra en el ejemplo siguiente.

Contract.EnsuresOnThrow<T>( this.F > 0 );

El argumento es la condición que debe ser true cada vez que se produce una excepción que es un subtipo de T.

Hay algunos tipos de excepción que son difíciles de utilizar en una condición posterior excepcional. Por ejemplo, el uso del tipo Exception para T exige que el método garantice la condición sin tener en cuenta el tipo de excepción que se produce, incluso si es un desbordamiento de pila u otra excepción imposible de controlar. Solo debe utilizar las condiciones posteriores excepcionales para excepciones concretas que se pueden producir al llamar a un miembro, por ejemplo, al producirse InvalidTimeZoneException para una llamada al método TimeZoneInfo.

Condiciones posteriores especiales

Los siguientes métodos solo se pueden utilizar dentro de condiciones posteriores:

Puede hacer referencia a valores devueltos de métodos en condiciones posteriores mediante la expresión Contract. Result<T>(), donde T se reemplaza por el tipo de valor devuelto del método. Cuando el compilador no puede deducir el tipo, debe proporcionarlo explícitamente. Por ejemplo, el compilador de C# no puede deducir los tipos para los métodos que no toman ningún argumento, de modo que se requiere la siguiente condición posterior: los métodos Contract.Ensures(0 < Contract.Result<int>()) con un tipo de valor devuelto de void no pueden hacer referencia a Contract. Result<T>() en sus condiciones posteriores.

Un valor preindicado en una condición posterior hace referencia al valor de una expresión en el inicio de un método o propiedad. Utiliza la expresión Contract.OldValue<T>(e), donde T es el tipo de e. Puede omitir el argumento de tipo genérico siempre que el compilador pueda deducir su tipo. (Por ejemplo, el compilador de C# siempre deduce el tipo porque toma un argumento.) Hay varias restricciones en lo que puede producirse en e y los contextos en los que puede aparecer una expresión antigua. Una expresión antigua no puede contener otra expresión antigua. Mucho más importante es que una expresión antigua debe hacer referencia a un valor que existía en el estado de la condición previa del método. En otras palabras, debe ser una expresión que se puede evaluar con tal de que la condición previa del método sea true. A continuación se muestran varias instancias de esta regla.

El valor debe existir en el estado de condición previa del método. Para hacer referencia a un campo en un objeto, las condiciones previas deben garantizar que ese objeto es siempre no null.
No puede hacer referencia al valor devuelto del método en una expresión antigua:
```
Contract.OldValue(Contract.Result<int>() + x) // ERROR
```
No puede hacer referencia a los parámetros out en una expresión antigua.
Una expresión antigua no puede depender de la variable enlazada de un cuantificador si el intervalo del cuantificador depende del valor devuelto del método:
```
Contract. ForAll (0,Contract. Result<int>(),
i => Contract.OldValue(xs[i]) > 3 ); // ERROR
```
Una expresión antigua no puede hacer referencia al parámetro del delegado anónimo en una llamada ForAll o Exists a menos que se utilice como indizador o argumento a una llamada al método:
```
Contract. ForAll (0, xs .Length, i => Contract.OldValue(xs[i]) > 3); // OK
Contract. ForAll (0, xs .Length, i => Contract.OldValue(i) > 3 ); // ERROR
```
Una expresión antigua no se puede producir en el cuerpo de un delegado anónimo si el valor de la expresión antigua depende de cualquiera de los parámetros del delegado anónimo, a menos que el delegado anónimo sea un argumento al método Exists o ForAll:
```
Method( ... (T t) => Contract.OldValue(... t ...) ... ); // ERROR
```

Los parámetros Out presentan un problema porque los contratos aparecen antes del cuerpo del método y la mayoría de los compiladores no permiten referencias a parámetros out en condiciones posteriores. Para resolver este problema, la clase Contract proporciona el método ValueAtReturn<T>, que permite una condición posterior basada en un parámetro out.

public void OutParam(out int x) f
Contract.Ensures(Contract.ValueAtReturn(out x) == 3);
x = 3;

Al igual que con el método OldValue<T>, puede omitir el parámetro de tipo genérico siempre que el compilador pueda deducir su tipo. El sistema de reescritura del contrato reemplaza la llamada al método por el valor del parámetro out. El método ValueAtReturn<T> solo puede aparecer en condiciones posteriores. El argumento al método debe ser un parámetro out o un campo de un parámetro out de estructura. Éste último también es útil al hacer referencia a campos en la condición posterior de un constructor de estructuras.

Nota
Actualmente, las herramientas de análisis de contrato de código no comprueban si los parámetros out se inicializan correctamente y no tienen en cuenta su mención en la condición posterior.Por consiguiente, en el ejemplo anterior, si la línea después del contrato hubiera utilizado el valor de x en lugar de asignarle un entero, un compilador no emitiría el error correcto.Sin embargo, en una compilación en la que no está definido el símbolo de preprocesador CONTRACTS FULL (como una compilación de lanzamiento), el compilador emitirá un error.

Actualmente, las herramientas de análisis de contrato de código no comprueban si los parámetros out se inicializan correctamente y no tienen en cuenta su mención en la condición posterior.Por consiguiente, en el ejemplo anterior, si la línea después del contrato hubiera utilizado el valor de x en lugar de asignarle un entero, un compilador no emitiría el error correcto.Sin embargo, en una compilación en la que no está definido el símbolo de preprocesador CONTRACTS FULL (como una compilación de lanzamiento), el compilador emitirá un error.

Invariables

Los objetos invariables son condiciones que deben ser verdad para cada instancia de una clase cada vez que ese objeto está visible para un cliente. Expresan las condiciones en las que se considera que el objeto es correcto.

Los métodos invariables se identifican marcándose con el atributo ContractInvariantMethodAttribute. Los métodos invariables no deben contener ningún código salvo una secuencia de llamadas al método Invariant, cada una de las cuales especifica una invariable individual, como se muestra en el siguiente ejemplo.

[ContractInvariantMethod]
protected void ObjectInvariant () 
{
Contract.Invariant ( this.y >= 0 );
Contract.Invariant ( this.x > this.y );
...
}

Las invariables están condicionalmente definidas por el símbolo de preprocesador CONTRACTS FULL. Durante la comprobación en tiempo de ejecución, las invariables se comprueban al final de cada método público. Si un invariable menciona un método público en la misma clase, la comprobación de la invariable que se produce normalmente al final de ese método público está deshabilitada. En su lugar, la comprobación solo se produce al final de la llamada al método más externo a esa clase. Esto también pasa si se vuelve a escribir la clase debido a una llamada a un método en otra clase. No se comprueban los finalizadores de objeto en las invariables ni ningún método que implemente el método Dispose.

Instrucciones de uso

Clasificación de contratos

La siguiente tabla muestra el orden de elementos que debe utilizar al escribir contratos de método.

If-then-throw statements	Condiciones previas públicas compatibles con versiones anteriores
Requires	Todas las condiciones previas públicas.
Ensures	Todas las condiciones posteriores públicas (normales).
EnsuresOnThrow	Todas las condiciones posteriores públicas excepcionales.
Ensures	Todas las condiciones posteriores privadas/internas (normales).
EnsuresOnThrow	Todas las condiciones posteriores privadas/internas excepcionales.
EndContractBlock	Si utiliza condiciones previas de estilo if-then-throw sin ningún otro contrato, llame a EndContractBlock para indicar que todas las comprobaciones "if" anteriores son condiciones previas.

Pureza

Todos los métodos a los que se llaman dentro de un contrato deben ser puros; es decir, no deben actualizar ningún estado preexistente. Un método puro puede modificar objetos creados después de la entrada en el método puro.

Las herramientas de contratos de código suponen que los siguientes elementos de código son puros:

Los métodos que están marcados con PureAttribute.
Los tipos que están marcados con PureAttribute (el atributo se aplica a los métodos de todo tipo).
Descriptores de acceso de propiedad get.
Operadores (métodos estáticos cuyos nombres comienzan por "op" y que tienen uno o dos parámetros y un tipo de valor devuelto no nulo).
Cualquier método cuyo nombre completo comience por "System.Diagnostics.Contracts.Contract", "System.String", "System.IO.Path" o "System.Type".
Cualquier delegado invocado, siempre que el tipo de delegado mismo tenga el atributo PureAttribute. Los tipos de delegado System.Predicate<T> y System.Comparison<T> se consideran puros.

Visibilidad

Todos los miembros mencionados en un contrato deben ser por lo menos tan visibles como el método en que aparecen. Por ejemplo, no se puede mencionar un campo privado en una condición previa para un método público; los clientes no pueden validar este tipo de contrato antes de llamar al método. Sin embargo, si el campo está marcado con ContractPublicPropertyNameAttribute, está eximido de cumplir estas reglas.

Ejemplo

En el siguiente ejemplo se muestra el uso de contratos de código.

Imports System
Imports System.Diagnostics.Contracts


' An IArray is an ordered collection of objects.    
<ContractClass(GetType(IArrayContract))> _
Public Interface IArray
    ' The Item property provides methods to read and edit entries in the array.

    Default Property Item(ByVal index As Integer) As [Object]


    ReadOnly Property Count() As Integer


    ' Adds an item to the list.  
    ' The return value is the position the new element was inserted in.
    Function Add(ByVal value As Object) As Integer

    ' Removes all items from the list.
    Sub Clear()

    ' Inserts value into the array at position index.
    ' index must be non-negative and less than or equal to the 
    ' number of elements in the array.  If index equals the number
    ' of items in the array, then value is appended to the end.
    Sub Insert(ByVal index As Integer, ByVal value As [Object])


    ' Removes the item at position index.
    Sub RemoveAt(ByVal index As Integer)
End Interface 'IArray

<ContractClassFor(GetType(IArray))> _
Friend MustInherit Class IArrayContract
    Implements IArray

    Function Add(ByVal value As Object) As Integer Implements IArray.Add
        ' Returns the index in which an item was inserted.
        Contract.Ensures(Contract.Result(Of Integer)() >= -1) '
        Contract.Ensures(Contract.Result(Of Integer)() < CType(Me, IArray).Count) '
        Return 0

    End Function 'IArray.Add

    Default Property Item(ByVal index As Integer) As Object Implements IArray.Item
        Get
            Contract.Requires(index >= 0)
            Contract.Requires(index < CType(Me, IArray).Count)
            Return 0 '
        End Get
        Set(ByVal value As [Object])
            Contract.Requires(index >= 0)
            Contract.Requires(index < CType(Me, IArray).Count)
        End Set
    End Property

    Public ReadOnly Property Count() As Integer Implements IArray.Count
        Get
            Contract.Requires(Count >= 0)
            Contract.Requires(Count <= CType(Me, IArray).Count)
            Return 0 '
        End Get
    End Property

    Sub Clear() Implements IArray.Clear
        Contract.Ensures(CType(Me, IArray).Count = 0)

    End Sub 'IArray.Clear


    Sub Insert(ByVal index As Integer, ByVal value As [Object]) Implements IArray.Insert
        Contract.Requires(index >= 0)
        Contract.Requires(index <= CType(Me, IArray).Count) ' For inserting immediately after the end.
        Contract.Ensures(CType(Me, IArray).Count = Contract.OldValue(CType(Me, IArray).Count) + 1)

    End Sub 'IArray.Insert


    Sub RemoveAt(ByVal index As Integer) Implements IArray.RemoveAt
        Contract.Requires(index >= 0)
        Contract.Requires(index < CType(Me, IArray).Count)
        Contract.Ensures(CType(Me, IArray).Count = Contract.OldValue(CType(Me, IArray).Count) - 1)

    End Sub 'IArray.RemoveAt
End Class 'IArrayContract

using System;
using System.Diagnostics.Contracts;

// An IArray is an ordered collection of objects.    
[ContractClass(typeof(IArrayContract))]
public interface IArray
{
    // The Item property provides methods to read and edit entries in the array.
    Object this[int index]
    {
        get;
        set;
    }

    int Count
    {
        get;

    }

    // Adds an item to the list.  
    // The return value is the position the new element was inserted in.
    int Add(Object value);

    // Removes all items from the list.
    void Clear();

    // Inserts value into the array at position index.
    // index must be non-negative and less than or equal to the 
    // number of elements in the array.  If index equals the number
    // of items in the array, then value is appended to the end.
    void Insert(int index, Object value);


    // Removes the item at position index.
    void RemoveAt(int index);
}

[ContractClassFor(typeof(IArray))]
internal abstract class IArrayContract : IArray
{
    int IArray.Add(Object value)
    {
        // Returns the index in which an item was inserted.
        Contract.Ensures(Contract.Result<int>() >= -1);
        Contract.Ensures(Contract.Result<int>() < ((IArray)this).Count);
        return default(int);
    }
    Object IArray.this[int index]
    {
        get
        {
            Contract.Requires(index >= 0);
            Contract.Requires(index < ((IArray)this).Count);
            return default(int);
        }
        set
        {
            Contract.Requires(index >= 0);
            Contract.Requires(index < ((IArray)this).Count);
        }
    }
    public int Count
    {
        get
        {
            Contract.Requires(Count >= 0);
            Contract.Requires(Count <= ((IArray)this).Count);
            return default(int);
        }
    }

    void IArray.Clear()
    {
        Contract.Ensures(((IArray)this).Count == 0);
    }

    void IArray.Insert(int index, Object value)
    {
        Contract.Requires(index >= 0);
        Contract.Requires(index <= ((IArray)this).Count);  // For inserting immediately after the end.
        Contract.Ensures(((IArray)this).Count == Contract.OldValue(((IArray)this).Count) + 1);
    }

    void IArray.RemoveAt(int index)
    {
        Contract.Requires(index >= 0);
        Contract.Requires(index < ((IArray)this).Count);
        Contract.Ensures(((IArray)this).Count == Contract.OldValue(((IArray)this).Count) - 1);
    }
}

Compartir a través de