Compartir a través de

Contratos de código (.NET Framework)

Nota:

Este artículo es específico de .NET Framework. No se aplica a implementaciones más recientes de .NET, incluidas .NET 6 y versiones posteriores.

Los contratos de código proporcionan una manera de especificar condiciones previas, condiciones posteriores y invariables de objetos en el código de .NET Framework. Las condiciones previas son requisitos que deben cumplirse al acceder a un método o una propiedad. Las condiciones posteriores describen las expectativas en el momento en que se cierra el código del método o propiedad. Las invariables de objeto describen el estado esperado de una clase que está en un buen estado.

Nota:

Los contratos de código no se admiten en .NET 5+ (incluidas las versiones de .NET Core). Considere usar tipos de referencia anulables en su lugar.

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. Las clases de contratos de código se encuentran en el espacio de nombres System.Diagnostics.Contracts.

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

  • Pruebas mejoradas: los contratos de código proporcionan comprobación de contratos estáticos, comprobación en tiempo de ejecución y generación de documentación.

  • Herramientas de pruebas automáticas: puede usar contratos de código para generar pruebas unitarias más significativas filtrando argumentos de prueba sin sentido que no cumplen las condiciones previas.

  • Comprobación estática: el comprobador estático puede decidir si hay infracciones de contrato sin ejecutar el programa. Comprueba si hay contratos implícitos, como desreferencias null y límites de matriz, 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. También hay hojas de estilos que se pueden usar con Sandcastle para que las páginas de documentación generadas tengan secciones de contrato.

Todos los lenguajes de .NET Framework pueden aprovechar inmediatamente los contratos; No es necesario escribir un analizador especial ni un compilador. Un complemento de Visual Studio le permite especificar el nivel de análisis de contratos de código que se va a realizar. Los analizadores pueden confirmar que los contratos tienen un formato correcto (comprobación de tipos y resolución de nombres) y pueden generar una forma compilada de los contratos en formato de lenguaje intermedio común (CIL). La creación de contratos en Visual Studio le permite aprovechar las ventajas de IntelliSense estándar proporcionada por la herramienta.

La mayoría de los métodos de la clase contract se compilan condicionalmente; Es decir, el compilador emite llamadas a estos métodos solo cuando se define un símbolo especial, CONTRACTS_FULL, mediante la #define directiva . CONTRACTS_FULL permite escribir contratos en su código sin usar directivas #ifdef; permite generar distintas compilaciones, algunas con contratos y otras sin ellos.

Para obtener herramientas e instrucciones detalladas para usar contratos de código, consulte Contratos de código en el sitio de Marketplace de Visual Studio.

Condiciones previas

Puede expresar condiciones previas mediante el Contract.Requires método . Las condiciones previas especifican el estado cuando se invoca un método. Por lo general, se usan para especificar valores de parámetro válidos. Todos los miembros mencionados en las precondiciones deben ser al menos tan accesibles como el propio método. De lo contrario, puede que los llamadores de un método no comprendan la precondición. La condición no debe tener efectos secundarios. El analizador en tiempo de ejecución determina el comportamiento en tiempo de ejecución de las precondiciones fallidas.

Por ejemplo, la siguiente condición previa expresa que el parámetro x debe ser distinto de null.

Contract.Requires(x != null);

Si el código debe producir una excepción determinada en caso de error de una condición previa, puede usar la sobrecarga genérica de Requires como se indica a continuación.

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

La herencia requiere instrucciones

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

  • Las instrucciones aparecen antes que cualquier otra instrucción en un método.

  • El conjunto completo de estas instrucciones va seguido de una llamada de método explícita a Contract, como una llamada al método Requires, Ensures, EnsuresOnThrow o EndContractBlock.

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

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

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

Condiciones posteriores

Las postcondiciones son contratos sobre el estado de un método cuando finaliza. La condición posterior se comprueba justo antes de salir de un método. El analizador de runtime determina el comportamiento en tiempo de ejecución de las condiciones posteriores con errores.

A diferencia de las condiciones previas, las condiciones posteriores pueden hacer referencia a los miembros con menos visibilidad. Es posible que un cliente no pueda comprender o usar 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 usar el método correctamente.

Condiciones posteriores estándar

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

Contract.Ensures(this.F > 0);

Condiciones posteriores excepcionales

Las condiciones posteriores excepcionales son condiciones posteriores que deben ser true cuando un método produce una excepción determinada. Puede especificar estas condiciones posteriores mediante el Contract.EnsuresOnThrow método , 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 de un subtipo de T .

Hay algunos tipos de excepciones que son difíciles de usar en una condición posterior excepcional. Por ejemplo, el uso del tipo Exception para T requiere que el método garantice la condición independientemente del tipo de excepción que se produzca, incluso si se trata de un desbordamiento de pila u otra excepción imposible de controlar. Debe usar condiciones posteriores excepcionales solo para excepciones específicas que se pueden producir cuando se invoca a un miembro, por ejemplo, cuando se lanza una excepción InvalidTimeZoneException durante una llamada al método TimeZoneInfo.

Condiciones posteriores especiales

Los métodos siguientes pueden usarse únicamente dentro de condiciones posteriores:

  • Puede hacer referencia a los valores devueltos del método en las 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 tipos para los métodos que no toman ningún argumento, por lo que requiere la siguiente condición postcondition: Contract.Ensures(0 <Contract.Result<int>()) Los métodos con un tipo de valor devuelto de void no pueden hacer referencia a Contract.Result<T>() en sus postconditions.

  • 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. Usa 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 sobre lo que puede ocurrir 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. Lo más importante es que una expresión antigua debe hacer referencia a un valor que existía en el estado de condición previa del método. En otras palabras, debe ser una expresión que se pueda evaluar siempre que la condición previa del método sea true. Estas son varias instancias de esa 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 el objeto siempre no sea NULL.

    • No se puede hacer referencia al valor devuelto del método en una expresión antigua:

      Contract.OldValue(Contract.Result<int>() + x) // ERROR

    • No se puede hacer referencia a out parámetros 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 ForAll llamada o Exists a menos que se use como indexador o argumento a una llamada de 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

    • No se puede producir una expresión antigua en el cuerpo de un delegado anónimo si el valor de la expresión anterior depende de cualquiera de los parámetros del delegado anónimo, a menos que el delegado anónimo sea un argumento para el ForAll método o Exists :

      Method(... (T t) => Contract.OldValue(... t ...) ...); // ERROR

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

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

      Al igual que con el OldValue método , 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 de método por el valor del parámetro out. El método ValueAtReturn solo aparece en las condiciones posteriores. El argumento del método debe ser un out parámetro o un campo de un parámetro de estructura out . Este último también es útil cuando se hace referencia a los campos de la condición posterior de un constructor de estructura.

      Nota:

      Actualmente, las herramientas de análisis de contratos de código no comprueban si out los parámetros se inicializan correctamente e ignoran su mención en la condición posterior. Por lo tanto, en el ejemplo anterior, si la línea después del contrato hubiera usado el valor de x en lugar de asignarle un entero, un compilador no generaría el error correcto. Sin embargo, en una compilación en la que el símbolo del preprocesador de CONTRACTS_FULL no está definido (por ejemplo, una compilación de versión), el compilador emitirá un error.

Invariantes

Las invariables de objeto son condiciones que deben ser verdaderas para cada instancia de una clase siempre que ese objeto sea visible para un cliente. Expresan las condiciones en las que el objeto se considera correcto.

Los métodos invariables se identifican marcando con el ContractInvariantMethodAttribute atributo . Los métodos invariables no deben contener código excepto una secuencia de llamadas al Invariant método , cada uno de los cuales especifica una invariable individual, como se muestra en el ejemplo siguiente.

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

Las invariables se definen condicionalmente mediante el símbolo del 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 una invariable menciona un método público en la misma clase, la comprobación invariable que normalmente se produciría al final de ese método público está deshabilitada. En su lugar, la comprobación solo se realiza al final de la llamada al método más exterior de esa clase. Esto también ocurre si la clase se vuelve a escribir debido a una llamada a un método en otra clase. Las invariables no se comprueban para un finalizador de objetos y una IDisposable.Dispose implementación.

Instrucciones de uso

Clasificación de contratos

En la tabla siguiente se muestra el orden de los elementos que debe usar 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 usa condiciones previas de estilo if-then-throw sin ningún otro contrato, coloque una llamada a EndContractBlock para indicar que todas las comprobaciones if anteriores son requisitos previos.

Pureza

Todos los métodos a los que se llama dentro de un contrato deben ser puros; es decir, no deben actualizar ningún estado preexistente. Se permite que un método puro modifique objetos que han sido creados después de la entrada en el método puro.

Actualmente, las herramientas de contrato de código suponen que los siguientes elementos de código son puros:

  • Métodos marcados con .PureAttribute

  • Tipos marcados con PureAttribute (el atributo se aplica a todos los métodos del tipo).

  • Descriptores de acceso get de propiedad.

  • 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 esté atribuido con el 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 al menos tan visibles como el método en el 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 contrato antes de llamar al método . Sin embargo, si el campo está marcado con ContractPublicPropertyNameAttribute, está exento de estas reglas.

Ejemplo

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

#define CONTRACTS_FULL

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);
    }
}

#Const CONTRACTS_FULL = True

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


    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


    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
End Class