Codecontracten (.NET Framework)

Notitie

Dit artikel is specifiek voor .NET Framework. Dit geldt niet voor nieuwere implementaties van .NET, waaronder .NET 6 en nieuwere versies.

Codecontracten bieden een manier om voorwaarden, postconditions en object-invarianten in .NET Framework-code op te geven. Voorwaarden zijn vereisten waaraan moet worden voldaan bij het invoeren van een methode of eigenschap. Postconditions beschrijven verwachtingen op het moment dat de methode of eigenschapscode wordt afgesloten. Objectinvarianten beschrijven de verwachte status voor een klasse die zich in een goede staat bevindt.

Notitie

Codecontracten worden niet ondersteund in .NET 5+ (inclusief .NET Core-versies). Overweeg in plaats daarvan null-referentietypen te gebruiken.

Codecontracten bevatten klassen voor het markeren van uw code, een statische analyse voor compileertijdanalyse en een runtime-analyse. De klassen voor codecontracten vindt u in de System.Diagnostics.Contracts naamruimte.

De voordelen van codecontracten zijn onder andere:

• Verbeterde tests: codecontracten bieden statische contractverificatie, runtimecontrole en het genereren van documentatie.

• Hulpprogramma's voor automatisch testen: u kunt codecontracten gebruiken om zinvollere eenheidstests te genereren door betekenisloze testargumenten te filteren die niet voldoen aan voorwaarden.

• Statische verificatie: De statische controle kan bepalen of er contractschendingen zijn zonder het programma uit te voeren. Er wordt gecontroleerd op impliciete contracten, zoals null-deducties en matrices, en expliciete contracten.

• Referentiedocumentatie: De documentatiegenerator verbetert bestaande XML-documentatiebestanden met contractinformatie. Er zijn ook opmaakmodellen die kunnen worden gebruikt met Sandcastle , zodat de gegenereerde documentatiepagina's contractsecties bevatten.

Alle .NET Framework-talen kunnen direct profiteren van contracten; u hoeft geen speciale parser of compiler te schrijven. Met een Visual Studio-invoegtoepassing kunt u opgeven welk niveau van codecontractanalyse moet worden uitgevoerd. De analyses kunnen bevestigen dat de contracten goed zijn gevormd (typecontrole en naamomzetting) en een gecompileerde vorm van de contracten kunnen produceren in een gemeenschappelijke tussentaal (CIL). Met het ontwerpen van contracten in Visual Studio kunt u profiteren van de standaardIntelliSense die door het hulpprogramma wordt geleverd.

De meeste methoden in de contractklasse worden voorwaardelijk gecompileerd; Dat wil gezegd: de compiler verzendt alleen aanroepen naar deze methoden wanneer u een speciaal symbool, CONTRACTS_FULL, definieert met behulp van de #define instructie. CONTRACTS_FULL kunt u contracten in uw code schrijven zonder gebruik te maken van #ifdef instructies. U kunt verschillende builds, sommige met contracten en sommige zonder maken.

Zie Code Contracts op de Site van Visual Studio Marketplace voor meer informatie over het gebruik van codecontracten en gedetailleerde instructies voor het gebruik van codecontracten .

Voorwaarden vooraf

U kunt voorwaarden uitdrukken met behulp van de Contract.Requires methode. Voorwaarden geven de status op wanneer een methode wordt aangeroepen. Ze worden over het algemeen gebruikt om geldige parameterwaarden op te geven. Alle leden die onder voorwaarden worden genoemd, moeten ten minste zo toegankelijk zijn als de methode zelf; anders wordt de voorwaarde mogelijk niet begrepen door alle aanroepers van een methode. De voorwaarde mag geen bijwerkingen hebben. Het runtimegedrag van mislukte voorwaarden wordt bepaald door de runtime-analyse.

De volgende voorwaarde geeft bijvoorbeeld aan dat de parameter x niet null moet zijn.

Contract.Requires(x != null);

Als uw code een bepaalde uitzondering moet genereren bij het mislukken van een voorwaarde, kunt u de algemene overbelasting als Requires volgt gebruiken.

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

Verouderde vereist instructies

De meeste code bevat een parametervalidatie in de vorm van if--thenthrow code. De contracttools herkennen deze instructies als voorwaarden in de volgende gevallen:

• De instructies worden weergegeven vóór andere instructies in een methode.

• De volledige set van dergelijke instructies wordt gevolgd door een expliciete Contract methodeaanroep, zoals een aanroep naar de Requires, Ensuresof EndContractBlockEnsuresOnThrowmethode.

Wanneer if--thenthrow instructies in dit formulier worden weergegeven, herkennen de hulpprogramma's deze als verouderde requires instructies. Als er geen andere contracten volgenif--thenthrow, beëindigt u de code met de Contract.EndContractBlock methode.

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

Houd er rekening mee dat de voorwaarde in de voorgaande test een ontkende voorwaarde is. (De werkelijke voorwaarde zou x != nullzijn .) Een ontkende voorwaarde is zeer beperkt: deze moet worden geschreven zoals in het vorige voorbeeld wordt weergegeven; dat wil zeggen, het mag geen else componenten bevatten en de hoofdtekst van de then component moet één throw instructie zijn. De if test is onderhevig aan zowel zuiverheidsregels als zichtbaarheidsregels (zie Gebruiksrichtlijnen), maar de throw expressie is alleen onderhevig aan zuiverheidsregels. Het type uitzondering dat wordt gegenereerd, moet echter zo zichtbaar zijn als de methode waarin het contract plaatsvindt.

Postconditions

Postconditions zijn contracten voor de status van een methode wanneer deze wordt beëindigd. De postcondition wordt vlak voor het afsluiten van een methode gecontroleerd. Het runtimegedrag van mislukte postconditions wordt bepaald door de runtime-analyse.

In tegenstelling tot voorwaarden kunnen postconditions verwijzen naar leden met minder zichtbaarheid. Een client kan mogelijk bepaalde informatie die wordt uitgedrukt door een postcondition met een privéstatus, niet begrijpen of gebruiken, maar dit heeft geen invloed op de mogelijkheid van de client om de methode correct te gebruiken.

Standaardpostconditions

U kunt standaardpostconditions uitdrukken met behulp van de Ensures methode. Postconditions drukken een voorwaarde uit die bij normale beëindiging van de methode moet zijn true .

Contract.Ensures(this.F > 0);

Uitzonderlijke postconditions

Uitzonderlijke postconditions zijn postconditions die moeten zijn true wanneer een bepaalde uitzondering wordt gegenereerd door een methode. U kunt deze postconditions opgeven met behulp van de Contract.EnsuresOnThrow methode, zoals in het volgende voorbeeld wordt weergegeven.

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

Het argument is de voorwaarde die moet zijn true wanneer een uitzondering die een subtype is, T wordt gegenereerd.

Er zijn enkele uitzonderingstypen die moeilijk te gebruiken zijn in een uitzonderlijke postcondition. Voor het gebruik van het type ExceptionT is bijvoorbeeld de methode vereist om de voorwaarde te garanderen, ongeacht het type uitzondering dat wordt gegenereerd, zelfs als het een stack-overloop of een andere onmogelijke controle-uitzondering is. U moet alleen uitzonderlijke postconditions gebruiken voor specifieke uitzonderingen die kunnen worden gegenereerd wanneer een lid wordt aangeroepen, bijvoorbeeld wanneer een InvalidTimeZoneException wordt gegenereerd voor een TimeZoneInfo methodeaanroep.

Speciale postconditions

De volgende methoden kunnen alleen binnen postconditions worden gebruikt:

• U kunt verwijzen naar retourwaarden van de methode in postconditions met behulp van de expressie Contract.Result<T>(), waarbij T deze wordt vervangen door het retourtype van de methode. Wanneer de compiler het type niet kan afleiden, moet u dit expliciet opgeven. De C#-compiler kan bijvoorbeeld geen typen afleiden voor methoden die geen argumenten gebruiken, dus hiervoor is de volgende postcondition vereist: Contract.Ensures(0 <Contract.Result<int>()) Methoden met een retourtype kunnen void niet verwijzen Contract.Result<T>() in hun postconditions.

• Een prestate-waarde in een postcondition verwijst naar de waarde van een expressie aan het begin van een methode of eigenschap. Hierbij wordt de expressie Contract.OldValue<T>(e)gebruikt, waarbij T het type eis. U kunt het algemene typeargument weglaten wanneer de compiler het type ervan kan afleiden. (De C#-compiler leidt bijvoorbeeld altijd het type af omdat er een argument wordt gebruikt.) Er zijn verschillende beperkingen voor wat er kan gebeuren e en de contexten waarin een oude expressie kan worden weergegeven. Een oude expressie kan geen andere oude expressie bevatten. Het belangrijkste is dat een oude expressie moet verwijzen naar een waarde die bestaat in de voorwaardestatus van de methode. Met andere woorden, het moet een expressie zijn die kan worden geëvalueerd zolang de voorwaarde van de methode is true. Hier volgen verschillende exemplaren van die regel.

  • De waarde moet bestaan in de voorwaardestatus van de methode. Om naar een veld op een object te verwijzen, moeten de voorwaarden garanderen dat het object altijd niet null is.

  • U kunt niet verwijzen naar de retourwaarde van de methode in een oude expressie:

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

  • U kunt niet verwijzen naar out parameters in een oude expressie.

  • Een oude expressie kan niet afhankelijk zijn van de afhankelijke variabele van een kwantificeerder als het bereik van de kwantificator afhankelijk is van de retourwaarde van de methode:

    Contract.ForAll(0, Contract.Result<int>(), i => Contract.OldValue(xs[i]) > 3); // ERROR
    

  • Een oude expressie kan niet verwijzen naar de parameter van de anonieme gemachtigde in een ForAll of Exists aanroep, tenzij deze wordt gebruikt als indexeerfunctie of argument voor een methodeaanroep:

    Contract.ForAll(0, xs.Length, i => Contract.OldValue(xs[i]) > 3); // OK
    Contract.ForAll(0, xs.Length, i => Contract.OldValue(i) > 3); // ERROR
    

  • Een oude expressie kan niet voorkomen in de hoofdtekst van een anonieme gemachtigde als de waarde van de oude expressie afhankelijk is van een van de parameters van de anonieme gemachtigde, tenzij de anonieme gemachtigde een argument is voor de ForAll of Exists methode:

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

  • Out parameters zijn een probleem omdat contracten worden weergegeven vóór de hoofdtekst van de methode en de meeste compilers geen verwijzingen out naar parameters in postconditions toestaan. Om dit probleem op te lossen, biedt de Contract klasse de ValueAtReturn methode, die een postcondition op basis van een out parameter toestaat.

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

    Net als bij de OldValue methode kunt u de algemene typeparameter weglaten wanneer de compiler het type ervan kan afleiden. De contractherschrijver vervangt de methode-aanroep door de waarde van de out parameter. De ValueAtReturn methode kan alleen in postconditions worden weergegeven. Het argument voor de methode moet een out parameter of een veld van een structuurparameter out zijn. De laatste is ook handig bij het verwijzen naar velden in de postcondition van een structuurconstructor.

    Notitie

    Momenteel controleren de hulpprogramma's voor het analyseren van codecontracten niet of out parameters correct worden geïnitialiseerd en worden ze genegeerd in de postcondition. Daarom, in het vorige voorbeeld, als de regel na het contract de waarde had gebruikt van x in plaats van een geheel getal toe te wijzen, zou een compiler de juiste fout niet uitgeven. In een build waarbij het CONTRACTS_FULL preprocessorsymbool niet is gedefinieerd (zoals een release-build), geeft de compiler echter een fout.

Invarianten

Objectinvarianten zijn voorwaarden die waar moeten zijn voor elk exemplaar van een klasse wanneer dat object zichtbaar is voor een client. Zij geven de voorwaarden aan waaronder het object als juist wordt beschouwd.

De invariante methoden worden geïdentificeerd door te worden gemarkeerd met het ContractInvariantMethodAttribute kenmerk. De invariante methoden mogen geen code bevatten, behalve voor een reeks aanroepen naar de Invariant methode, die elk een afzonderlijke invariant specificeert, zoals wordt weergegeven in het volgende voorbeeld.

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

Invarianten worden voorwaardelijk gedefinieerd door het CONTRACTS_FULL preprocessorsymbool. Tijdens de uitvoeringscontrole worden invarianten aan het einde van elke openbare methode gecontroleerd. Als een invariant een openbare methode vermeldt in dezelfde klasse, wordt de invariante controle die normaal gesproken aan het einde van die openbare methode zou plaatsvinden uitgeschakeld. In plaats daarvan vindt de controle alleen plaats aan het einde van de buitenste methode-aanroep naar die klasse. Dit gebeurt ook als de klasse opnieuw wordt ingevoerd vanwege een aanroep naar een methode in een andere klasse. Invarianten worden niet gecontroleerd op een object finalizer en een IDisposable.Dispose implementatie.

Gebruiksrichtlijnen

Contractvolgorde

In de volgende tabel ziet u de volgorde van elementen die u moet gebruiken bij het schrijven van methodecontracten.

If-then-throw statements	Achterwaarts compatibele openbare voorwaarden
Requires	Alle openbare voorwaarden.
Ensures	Alle openbare (normale) postconditions.
EnsuresOnThrow	Alle openbare uitzonderlijke postconditions.
Ensures	Alle privé/interne (normale) postconditions.
EnsuresOnThrow	Alle privé/interne uitzonderlijke postconditions.
EndContractBlock	Als u if--thenthrow voorwaarden voor stijl zonder andere contracten gebruikt, moet u een oproep plaatsen om aan te EndContractBlock geven dat alle voorgaande voorwaarden zijn als controles voorwaarden zijn.

Zuiverheid

Alle methoden die binnen een contract worden aangeroepen, moeten puur zijn; Dat wil gezegd, ze mogen geen bestaande status bijwerken. Een pure methode is toegestaan om objecten te wijzigen die zijn gemaakt na invoer in de pure methode.

Codecontracthulpprogramma's gaan er momenteel vanuit dat de volgende code-elementen puur zijn:

• Methoden die zijn gemarkeerd met de PureAttribute.

• Typen die zijn gemarkeerd met het PureAttribute kenmerk (het kenmerk is van toepassing op alle methoden van het type).

• Eigenschap get accessors.

• Operators (statische methoden waarvan de namen beginnen met op en die een of twee parameters en een niet-ongeldig retourtype hebben).

• Elke methode waarvan de volledig gekwalificeerde naam begint met System.Diagnostics.Contracts.Contract, System.String, System.IO.Path of System.Type.

• Elke aangeroepen gemachtigde, mits het type gemachtigde zelf wordt toegeschreven aan de PureAttribute. De gedelegeerdentypen System.Predicate<T> en System.Comparison<T> worden beschouwd als puur.

Visibility

Alle leden die in een contract worden genoemd, moeten minstens zo zichtbaar zijn als de methode waarin ze worden weergegeven. Een privéveld kan bijvoorbeeld niet worden vermeld in een voorwaarde voor een openbare methode; clients kunnen een dergelijk contract niet valideren voordat ze de methode aanroepen. Als het veld echter is gemarkeerd met het ContractPublicPropertyNameAttributeveld, is het uitgesloten van deze regels.

Opmerking

In het volgende voorbeeld ziet u het gebruik van codecontracten.

#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