Dela via

Kodkontrakt (.NET Framework)

  • Artikel

Kommentar

Den här artikeln är specifik för .NET Framework. Det gäller inte för nyare implementeringar av .NET, inklusive .NET 6 och senare versioner.

Kodkontrakt är ett sätt att ange förhandsvillkor, postkonditioner och objektvarianter i .NET Framework-kod. Förhandsvillkor är krav som måste uppfyllas när du anger en metod eller egenskap. Postconditions beskriver förväntningar när metoden eller egenskapskoden avslutas. Objektvarianter beskriver det förväntade tillståndet för en klass som är i ett bra tillstånd.

Kommentar

Kodkontrakt stöds inte i .NET 5+ (inklusive .NET Core-versioner). Överväg att använda null-referenstyper i stället.

Kodkontrakt innehåller klasser för att markera din kod, en statisk analys för kompileringstidsanalys och en körningsanalys. Klasserna för kodkontrakt finns i System.Diagnostics.Contracts namnområdet.

Fördelarna med kodkontrakt är följande:

  • Förbättrad testning: Kodkontrakt ger statisk kontraktsverifiering, körningskontroll och generering av dokumentation.

  • Automatiska testverktyg: Du kan använda kodkontrakt för att generera mer meningsfulla enhetstester genom att filtrera bort meningslösa testargument som inte uppfyller förhandsvillkoren.

  • Statisk verifiering: Den statiska kontrollen kan avgöra om det finns några kontraktsöverträdelser utan att köra programmet. Den söker efter implicita kontrakt, till exempel null-avreferenser och matrisgränsvärden och explicita kontrakt.

  • Referensdokumentation: Dokumentationsgeneratorn utökar befintliga XML-dokumentationsfiler med kontraktsinformation. Det finns även formatmallar som kan användas med Sandcastle så att de genererade dokumentationssidorna har kontraktavsnitt.

Alla .NET Framework-språk kan omedelbart dra nytta av kontrakt. du behöver inte skriva en särskild parser eller kompilator. Med ett Visual Studio-tillägg kan du ange vilken nivå av kodkontraktsanalys som ska utföras. Analysverktygen kan bekräfta att kontrakten är välformulerade (typkontroll och namnmatchning) och kan skapa en kompilerad form av kontrakten i CIL-format (common intermediate language). Med redigeringskontrakt i Visual Studio kan du dra nytta av den Standard IntelliSense som tillhandahålls av verktyget.

De flesta metoder i kontraktsklassen kompileras villkorligt. Kompilatorn sänder bara ut anrop till dessa metoder när du definierar en särskild symbol, CONTRACTS_FULL, med hjälp #define av direktivet. CONTRACTS_FULL kan du skriva kontrakt i koden utan att använda #ifdef direktiv. Du kan skapa olika versioner, vissa med kontrakt och andra utan.

Verktyg och detaljerade instruktioner för att använda kodkontrakt finns i Kodkontrakt på Webbplatsen för Visual Studio Marketplace.

Förvillkor

Du kan uttrycka förhandsvillkor med hjälp Contract.Requires av metoden . Förhandsvillkor anger tillstånd när en metod anropas. De används vanligtvis för att ange giltiga parametervärden. Alla medlemmar som nämns i förhandsvillkor måste vara minst lika tillgängliga som själva metoden. annars kanske inte alla som anropar en metod förstår förhandsvillkoret. Villkoret får inte ha några biverkningar. Körningsbeteendet för misslyckade förhandsvillkor bestäms av körningsanalysatorn.

Följande villkor uttrycker till exempel att parametern x måste vara icke-null.

Contract.Requires(x != null);

Om koden måste utlösa ett visst undantag vid fel i en förhandsvillkor kan du använda den allmänna överbelastningen på Requires följande sätt.

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

Äldre kräver instruktioner

De flesta kod innehåller viss parameterverifiering i form av if--thenthrow kod. Kontraktsverktygen identifierar dessa instruktioner som förhandsvillkor i följande fall:

När if--thenthrow instruktioner visas i det här formuläret identifierar verktygen dem som äldre requires instruktioner. Om inga andra kontrakt följer sekvensen if--thenthrow avslutar du koden med Contract.EndContractBlock -metoden.

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

Observera att villkoret i föregående test är en negerad förutsättning. (Den faktiska förutsättningen skulle vara x != null.) En negerad förutsättning är mycket begränsad: Den måste skrivas enligt föregående exempel. det vill: den ska inte innehålla några else satser, och brödtexten i then satsen måste vara en enda throw instruktion. Testet if omfattas av både renhets- och synlighetsregler (se användningsriktlinjer), men throw uttrycket omfattas endast av renhetsregler. Typen av undantag måste dock vara lika synlig som den metod där kontraktet sker.

Postconditions

Postconditions är kontrakt för tillståndet för en metod när den avslutas. Postkonditionen kontrolleras precis innan en metod avslutas. Körningsbeteendet för misslyckade postkonditioner bestäms av körningsanalysatorn.

Till skillnad från förhandsvillkor kan postkonditioner referera till medlemmar med mindre synlighet. En klient kanske inte kan förstå eller använda viss information som uttrycks i en postkondition med privat tillstånd, men detta påverkar inte klientens möjlighet att använda metoden korrekt.

Standard Postconditions

Du kan uttrycka standard postconditions med hjälp Ensures av metoden . Postconditions uttrycker ett villkor som måste vara true vid normal avslutning av metoden.

Contract.Ensures(this.F > 0);

Exceptionella efterkonditioner

Exceptionella postkonditioner är postkonditioner som bör vara true när ett visst undantag genereras av en metod. Du kan ange dessa postconditions med hjälp Contract.EnsuresOnThrow av metoden, som följande exempel visar.

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

Argumentet är det villkor som måste vara true när ett undantag som är en undertyp av T genereras.

Det finns vissa undantagstyper som är svåra att använda i en exceptionell efterkondition. Om du till exempel använder typen Exception för krävs metoden för T att garantera villkoret oavsett vilken typ av undantag som utlöses, även om det är ett stackspill eller något annat undantag som är omöjligt att kontrollera. Du bör endast använda exceptionella postkonditioner för specifika undantag som kan genereras när en medlem anropas, till exempel när en InvalidTimeZoneException genereras för ett TimeZoneInfo metodanrop.

Särskilda postkonditioner

Följande metoder får endast användas inom efterkonditioner:

  • Du kan referera till metodreturvärden i postconditions med uttrycket Contract.Result<T>(), där T ersätts av metodens returtyp. När kompilatorn inte kan härleda typen måste du uttryckligen ange den. C#-kompilatorn kan till exempel inte härleda typer för metoder som inte tar några argument, så det kräver följande postcondition: Contract.Ensures(0 <Contract.Result<int>()) Metoder med returtypen void kan inte referera till Contract.Result<T>() i sina postkonditioner.

  • Ett prestate-värde i en postkondition refererar till värdet för ett uttryck i början av en metod eller egenskap. Det använder uttrycket Contract.OldValue<T>(e), där T är typen av e. Du kan utelämna argumentet för allmän typ när kompilatorn kan härleda sin typ. (C#-kompilatorn härleder till exempel alltid typen eftersom den tar ett argument.) Det finns flera begränsningar för vad som kan inträffa i e och de sammanhang där ett gammalt uttryck kan visas. Ett gammalt uttryck får inte innehålla ett annat gammalt uttryck. Viktigast av allt är att ett gammalt uttryck måste referera till ett värde som fanns i metodens villkorstillstånd. Med andra ord måste det vara ett uttryck som kan utvärderas så länge metodens förhandsvillkor är true. Här är flera instanser av regeln.

    • Värdet måste finnas i metodens villkorstillstånd. För att kunna referera till ett fält i ett objekt måste förhandsvillkoren garantera att objektet alltid inte är null.

    • Du kan inte referera till metodens returvärde i ett gammalt uttryck:

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

    • Du kan inte referera till out parametrar i ett gammalt uttryck.

    • Ett gammalt uttryck kan inte vara beroende av den bundna variabeln för en kvantifierare om kvantifierarens intervall är beroende av metodens returvärde:

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

    • Ett gammalt uttryck kan inte referera till parametern för det anonyma ombudet i ett ForAll eller Exists -anrop om det inte används som indexerare eller argument till ett metodanrop:

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

    • Ett gammalt uttryck kan inte förekomma i brödtexten för ett anonymt ombud om värdet för det gamla uttrycket är beroende av någon av parametrarna för det anonyma ombudet, såvida inte den anonyma delegaten ForAll är ett argument till metoden eller Exists :

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

    • Out parametrar utgör ett problem eftersom kontrakt visas före metodens brödtext och de flesta kompilatorer tillåter inte referenser till out parametrar i postkonditioner. För att lösa det här problemet Contract tillhandahåller ValueAtReturn klassen metoden, som tillåter en postcondition baserat på en out parameter.

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

      Precis som OldValue med metoden kan du utelämna den generiska typparametern när kompilatorn kan härleda dess typ. Kontraktrewriter ersätter metodanropet med värdet för parametern out . Metoden ValueAtReturn kan bara visas i postkonditioner. Argumentet till metoden måste vara en out parameter eller ett fält i en strukturparameter out . Det senare är också användbart när du refererar till fält i postkonditionen för en strukturkonstruktor.

      Kommentar

      För närvarande kontrollerar inte verktygen för kodkontraktsanalys om out parametrar initieras korrekt och bortser från deras omnämnande i efterkonditionen. Om raden efter kontraktet hade använt värdet x för i stället för att tilldela ett heltal till det i föregående exempel, skulle en kompilator därför inte utfärda rätt fel. I en version där symbolen för CONTRACTS_FULL förprocessor inte har definierats (till exempel en versionsversion) kommer kompilatorn dock att utfärda ett fel.

Invariants

Objektvarianter är villkor som ska vara sanna för varje instans av en klass när objektet är synligt för en klient. De uttrycker de villkor under vilka objektet anses vara korrekt.

De invarianta metoderna identifieras genom att markeras med attributet ContractInvariantMethodAttribute . De invarianta metoderna får inte innehålla någon kod förutom en sekvens med anrop till Invariant metoden, som var och en anger en enskild invariant, som visas i följande exempel.

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

Invarianter definieras villkorligt av symbolen CONTRACTS_FULL förprocessor. Under körningskontroll kontrolleras invarianter i slutet av varje offentlig metod. Om en invariant nämner en offentlig metod i samma klass inaktiveras den invarianta kontroll som normalt skulle inträffa i slutet av den offentliga metoden. I stället sker kontrollen endast i slutet av det yttersta metodanropet till den klassen. Detta inträffar också om klassen anges på nytt på grund av ett anrop till en metod i en annan klass. Invarianter kontrolleras inte för en objektfinaliserare och en IDisposable.Dispose implementering.

Användningsriktlinjer

Beställning av kontrakt

I följande tabell visas ordningen på de element som du bör använda när du skriver metodkontrakt.

If-then-throw statements Bakåtkompatibla offentliga förutsättningar
Requires Alla offentliga förutsättningar.
Ensures Alla offentliga (normala) postconditions.
EnsuresOnThrow Alla offentliga exceptionella postconditions.
Ensures Alla privata/interna (normala) postconditions.
EnsuresOnThrow Alla privata/interna exceptionella postconditions.
EndContractBlock Om du använder if--thenthrow stilförutsättningar utan andra kontrakt kan du anropa för EndContractBlock att ange att alla tidigare om kontroller är förhandsvillkor.

Renhet

Alla metoder som anropas inom ett kontrakt måste vara rena. Det vill säga att de inte får uppdatera något befintligt tillstånd. En ren metod tillåts att ändra objekt som har skapats efter posten i den rena metoden.

Verktyg för kodkontrakt förutsätter för närvarande att följande kodelement är rena:

  • Metoder som är markerade med PureAttribute.

  • Typer som är markerade med PureAttribute (attributet gäller för alla typer av metoder).

  • Egenskapen hämtar accessorer.

  • Operatorer (statiska metoder vars namn börjar med "op" och som har en eller två parametrar och en icke-void returtyp).

  • Alla metoder vars fullständigt kvalificerade namn börjar med "System.Diagnostics.Contracts.Contract", "System.String", "System.IO.Path" eller "System.Type".

  • Alla anropade ombud, förutsatt att själva ombudstypen tillskrivs PureAttribute. De delegerade typerna System.Predicate<T> och System.Comparison<T> betraktas som rena.

Synlighet

Alla medlemmar som nämns i ett kontrakt måste vara minst lika synliga som den metod där de visas. Ett privat fält kan till exempel inte nämnas i en förutsättning för en offentlig metod. klienter kan inte verifiera ett sådant kontrakt innan de anropar metoden. Men om fältet är markerat med ContractPublicPropertyNameAttributeär det undantaget från dessa regler.

Exempel

I följande exempel visas användningen av kodkontrakt.

#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