Codeverträge (.NET Framework)

Hinweis

Dieser Artikel ist spezifisch für .NET Framework. Sie gilt nicht für neuere Implementierungen von .NET, einschließlich .NET 6 und höherer Versionen.

Codeverträge bieten eine Möglichkeit zum Angeben von Vorbedingungen, Postconditionen und Objektinvarianten in .NET Framework-Code. Voraussetzungen sind Anforderungen, die beim Eingeben einer Methode oder Eigenschaft erfüllt werden müssen. Postconditions beschreiben die Erwartungen zum Zeitpunkt des Beendens der Methode oder des Eigenschaftencodes. Objektinvarianten beschreiben den erwarteten Zustand für eine Klasse, die sich in einem guten Zustand befindet.

Hinweis

Codeverträge werden in .NET 5+ (einschließlich .NET Core-Versionen) nicht unterstützt. Erwägen Sie stattdessen die Verwendung nullabler Verweistypen .

Codeverträge umfassen Klassen zum Markieren des Codes, einen statischen Analyzer für die Kompilierungszeitanalyse und einen Laufzeitanalysator. Die Klassen für Codeverträge finden Sie im System.Diagnostics.Contracts Namespace.

Zu den Vorteilen von Codeverträgen gehören:

• Verbesserte Tests: Codeverträge bieten statische Vertragsüberprüfung, Laufzeitüberprüfung und Dokumentationsgenerierung.

• Automatische Testtools: Sie können Codeverträge verwenden, um aussagekräftigere Komponententests zu generieren, indem Sie sinnlose Testargumente herausfiltern, die keine Voraussetzungen erfüllen.

• Statische Überprüfung: Die statische Überprüfung kann entscheiden, ob Vertragsverletzungen bestehen, ohne das Programm auszuführen. Er überprüft implizite Verträge, z. B. Null-Ableitungen und Arraygrenzen und explizite Verträge.

• Referenzdokumentation: Der Dokumentationsgenerator erweitert vorhandene XML-Dokumentationsdateien mit Vertragsinformationen. Es gibt auch Stylesheets, die mit Sandcastle verwendet werden können, sodass die generierten Dokumentationsseiten Über Vertragsabschnitte verfügen.

Alle .NET Framework-Sprachen können sofort die Vorteile von Verträgen nutzen; Sie müssen keinen speziellen Parser oder Compiler schreiben. Mit einem Visual Studio-Add-In können Sie die Ebene der auszuführenden Codevertragsanalyse angeben. Die Analysegeräte können bestätigen, dass die Verträge wohlgeformt sind (Typüberprüfung und Namensauflösung) und eine kompilierte Form der Verträge im CIL-Format (Common Intermediate Language) erzeugen können. Mit der Erstellung von Verträgen in Visual Studio können Sie den vom Tool bereitgestellten IntelliSense-Standard nutzen.

Die meisten Methoden in der Vertragsklasse werden bedingt kompiliert; d. h., der Compiler gibt Aufrufe dieser Methoden nur aus, wenn Sie mithilfe der #define Direktive ein spezielles Symbol CONTRACTS_FULL definieren. Mit CONTRACTS_FULL können Sie Verträge in Ihren Code schreiben, ohne #ifdef Direktiven zu verwenden; Sie können verschiedene Builds erstellen, einige mit Verträgen und einige ohne.

Tools und detaillierte Anweisungen für die Verwendung von Codeverträgen finden Sie unter Codeverträge auf der Visual Studio Marketplace-Website.

Vorbedingungen

Mit der Contract.Requires Methode können Sie Voraussetzungen ausdrücken. Voraussetzungen geben den Zustand an, wenn eine Methode aufgerufen wird. Sie werden in der Regel verwendet, um gültige Parameterwerte anzugeben. Alle Mitglieder, die in Voraussetzungen erwähnt werden, müssen mindestens so zugänglich sein wie die Methode selbst; andernfalls kann die Voraussetzung nicht von allen Aufrufern einer Methode verstanden werden. Die Bedingung darf keine Nebenwirkungen haben. Das Laufzeitverhalten der fehlgeschlagenen Vorbedingungen wird durch den Laufzeitanalysator bestimmt.

Die folgende Vorbedingung gibt z. B. an, dass der Parameter x ungleich NULL sein muss.

Contract.Requires(x != null);

Wenn Ihr Code eine bestimmte Ausnahme beim Fehlschlagen einer Vorbedingung auslösen muss, können Sie die generische Überladung Requires wie folgt verwenden.

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

Legacy erfordert Erklärungen

Der meiste Code enthält einige Parameterüberprüfungen in Form von if-then-throw Code. Die Vertragstools erkennen diese Aussagen in den folgenden Fällen als Voraussetzungen an:

• Die Anweisungen werden vor allen anderen Anweisungen in einer Methode angezeigt.

• Der gesamte Satz solcher Anweisungen folgt einem expliziten Contract Methodenaufruf, z. B. einem Aufruf der Requires, Ensures, , EnsuresOnThrowoder EndContractBlock Methode.

Wenn if-then-throw Anweisungen in dieser Form angezeigt werden, erkennen die Tools sie als Legacy-Anweisungen.requires Wenn keine anderen Verträge der if-then-throw Sequenz folgen, beenden Sie den Code mit der Contract.EndContractBlock Methode.

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

Beachten Sie, dass die Bedingung im vorherigen Test eine negierte Voraussetzung ist. (Die tatsächliche Voraussetzung wäre x != null.) Eine negierte Voraussetzung ist stark eingeschränkt: Sie muss wie im vorherigen Beispiel beschrieben geschrieben werden; d. h., sie sollte keine else Klauseln enthalten, und der Textkörper der then Klausel muss eine einzelne throw Anweisung sein. Der if Test unterliegt sowohl Reinheits- als auch Sichtbarkeitsregeln (siehe Nutzungsrichtlinien), aber der throw Ausdruck unterliegt nur Reinheitsregeln. Der Typ der ausgelösten Ausnahme muss jedoch genauso sichtbar sein wie die Methode, in der der Vertrag vorkommt.

Nachbedingungen

Nachbedingungen sind Verträge für den Zustand einer Methode, wenn diese beendet wird. Die Nachbedingung wird unmittelbar vor dem Beenden einer Methode überprüft. Das Laufzeitverhalten fehlgeschlagener Postconditionen wird vom Laufzeitanalysetool bestimmt.

Im Gegensatz zu Vorbedingungen können Nachbedingungen auf Mitglieder mit geringerer Sichtbarkeit verweisen. Ein Client ist möglicherweise nicht in der Lage, einige der Informationen zu verstehen oder zu verwenden, die durch eine Nachbedingung mithilfe eines privaten Zustands ausgedrückt wurden. Dadurch wird die Fähigkeit des Clients, die Methode ordnungsgemäß zu verwenden, jedoch nicht beeinträchtigt.

Standardmäßige Nachbedingungen

Sie können Standardmäßige Postconditionen mithilfe der Ensures Methode ausdrücken. Nachbedingungen drücken eine Bedingung aus, die bei normaler Beendigung der Methode true sein muss.

Contract.Ensures(this.F > 0);

Außergewöhnliche Postbedingungen

Ausnahmenachbedingungen sind Nachbedingungen, die true sein sollten, wenn eine bestimmte Ausnahme von einer Methode ausgelöst wird. Sie können diese Postconditionen mithilfe der Contract.EnsuresOnThrow Methode angeben, wie im folgenden Beispiel gezeigt.

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

Das Argument ist die Bedingung, die true sein muss, wenn eine Ausnahme ausgelöst wird, bei der es sich um einen Untertyp von T handelt.

Es gibt einige Ausnahmetypen, die in einer außergewöhnlichen Postcondition schwer zu verwenden sind. Die Verwendung des Typs Exception für T erfordert beispielsweise, dass die Methode die Bedingung unabhängig vom ausgelösten Ausnahmetyp garantiert, selbst wenn es sich um einen Stapelüberlauf oder eine andere nicht kontrollierbare Ausnahme handelt. Verwenden Sie Ausnahmenachbedingungen nur für bestimmte Ausnahmen, die beim Aufruf eines Members ausgelöst werden könnten, z. B. wenn eine InvalidTimeZoneException für einen TimeZoneInfo-Methodenaufruf ausgelöst wird.

Besondere Nachbedingungen

Die folgenden Methoden können nur innerhalb von Nachbedingungen verwendet werden:

• Sie können auf Methodenrückgabewerte in Postconditions verweisen, indem Sie den Ausdruck Contract.Result<T>() verwenden, wobei T durch den Rückgabetyp der Methode ersetzt wird. Wenn der Compiler den Typ nicht ableiten kann, müssen Sie ihn explizit angeben. Der C#-Compiler kann z. B. keine Typen für Methoden ableiten, die keine Argumente verwenden, daher ist die folgende Nachbedingung erforderlich: Contract.Ensures(0 <Contract.Result<int>()) Methoden mit einem Rückgabetyp von void können in ihren Nachbedingungen Contract.Result<T>() nicht referenziert werden.

• Ein prestate-Wert in einer Nachbedingung verweist auf den Wert eines Ausdrucks am Anfang einer Methode oder Eigenschaft. Er verwendet den Ausdruck Contract.OldValue<T>(e), wobei T der Typ von e. Sie können das generische Typargument weglassen, wenn der Compiler seinen Typ ableiten kann. (Der C#-Compiler leitet z. B. immer den Typ ab, da es ein Argument akzeptiert.) Es gibt mehrere Einschränkungen, was in e und in den Kontexten auftreten kann, in denen ein alter Ausdruck angezeigt werden kann. Ein alter Ausdruck darf keinen anderen alten Ausdruck enthalten. Vor allem muss ein alter Ausdruck auf einen Wert verweisen, der im Bedingungszustand der Methode vorhanden ist. Mit anderen Worten, es muss ein Ausdruck sein, der ausgewertet werden kann, solange die Voraussetzung der Methode ist true. Hier sind mehrere Beispiele für diese Regel.

  • Der Wert muss im Bedingungszustand der Methode vorhanden sein. Um auf ein Feld eines Objekts zu verweisen, müssen die Voraussetzungen garantieren, dass das Objekt immer nicht null ist.

  • Sie können nicht auf den Rückgabewert der Methode in einem alten Ausdruck verweisen:

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

  • Sie können in einem alten Ausdruck nicht auf Parameter verweisen out .

  • Ein alter Ausdruck kann nicht von der gebundenen Variablen eines Quantifizierers abhängen, wenn der Bereich des Quantifizierers vom Rückgabewert der Methode abhängt:

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

  • Ein alter Ausdruck kann nicht auf den Parameter des anonymen Delegaten in einem ForAll Oder Exists Aufruf verweisen, es sei denn, er wird als Indexer oder Argument für einen Methodenaufruf verwendet:

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

  • Ein alter Ausdruck kann nicht im Textkörper eines anonymen Delegaten auftreten, wenn der Wert des alten Ausdrucks von einem der Parameter des anonymen Delegaten abhängt, es sei denn, der anonyme Delegate ist ein Argument für die ForAll oder Exists Methode:

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

  • Out Parameter stellen ein Problem dar, da Verträge vor dem Textkörper der Methode angezeigt werden, und die meisten Compiler lassen keine Verweise auf out Parameter in postconditions zu. Um dieses Problem zu lösen, stellt die Contract Klasse die ValueAtReturn Methode bereit, die eine Postcondition basierend auf einem out Parameter zulässt.

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

    Wie bei der OldValue Methode können Sie den generischen Typparameter weglassen, wenn der Compiler seinen Typ ableiten kann. Der Contract-Rewriter ersetzt den Methodenaufruf durch den Wert des Parameters out. Die ValueAtReturn-Methode kann nur in Nachbedingungen angezeigt werden. Das Argument für die Methode muss ein out Parameter oder ein Feld eines Strukturparameters out sein. Letzteres ist auch hilfreich, wenn auf Felder in der Nachbedingung eines Strukturkonstruktors verwiesen wird.

    Hinweis

    Derzeit überprüfen die Codevertragsanalysetools nicht, ob out Parameter ordnungsgemäß initialisiert werden und ihre Erwähnung in der Postcondition ignorieren. Wenn daher im vorherigen Beispiel die Zeile nach dem Vertrag den Wert x verwendet hat, anstatt ihm eine ganze Zahl zuzuweisen, würde ein Compiler den richtigen Fehler nicht ausstellen. Bei einem Build, bei dem das CONTRACTS_FULL Präprozessorsymbol nicht definiert ist (z. B. ein Releasebuild), gibt der Compiler jedoch einen Fehler aus.

Invarianten

Objektinvarianten sind Bedingungen, die für jede Instanz einer Klasse erfüllt sein sollten, wenn dieses Objekt für einen Client sichtbar ist. Sie geben die Bedingungen an, unter denen das Objekt als korrekt betrachtet wird.

Die invarianten Methoden werden durch Kennzeichnung mit dem ContractInvariantMethodAttribute Attribut identifiziert. Die invarianten Methoden dürfen keinen Code enthalten, mit Ausnahme einer Abfolge von Aufrufen der Invariant Methode, von denen jede eine einzelne Invariante angibt, wie im folgenden Beispiel gezeigt.

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

Invarianten werden durch das CONTRACTS_FULL Präprozessorsymbol bedingt definiert. Während der Laufzeitüberprüfung werden Invarianten am Ende jeder öffentlichen Methode überprüft. Wenn eine Invariante in derselben Klasse eine öffentliche Methode erwähnt, wird die Invariantenüberprüfung, die normalerweise am Ende dieser öffentlichen Methode durchgeführt wird, deaktiviert. Stattdessen erfolgt die Überprüfung nur am Ende des äußersten Methodenaufrufs für diese Klasse. Dies geschieht auch, wenn die Klasse aufgrund eines Aufrufs einer Methode für eine andere Klasse erneut eingegeben wird. Invarianten werden auf einen Objektfinalizer und eine IDisposable.Dispose Implementierung nicht überprüft.

Verwendungsrichtlinien

Verträge – Reihenfolge

Die folgende Tabelle zeigt die Reihenfolge der Elemente, die Sie beim Schreiben von Methodenverträgen verwenden sollten.

If-then-throw statements	Abwärtskompatible öffentliche Vorbedingungen
Requires	Alle öffentlichen Voraussetzungen.
Ensures	Alle öffentlichen (normalen) Nachbedingungen
EnsuresOnThrow	Alle öffentlichen Ausnahmenachbedingungen
Ensures	Alle privaten/internen (normalen) Nachbedingungen
EnsuresOnThrow	Alle privaten/internen Ausnahmenachbedingungen
EndContractBlock	Rufen Sie bei Verwendung von if-then-throw-Formatvorbedingungen ohne andere Verträge EndContractBlock auf, um anzugeben, dass es sich bei allen vorherigen If-Überprüfungen um Vorbedingungen handelt.

Reinheit

Alle Methoden, die in einem Vertrag aufgerufen werden, müssen rein sein; d. h., sie dürfen keinen bereits vorhandenen Zustand aktualisieren. Eine reine Methode darf Objekte ändern, die nach dem Eintrag in die reine Methode erstellt wurden.

Codevertragstools gehen derzeit davon aus, dass die folgenden Codeelemente rein sind:

• Methoden, die mit dem PureAttribute markiert sind.

• Typen, die mit dem PureAttribute Attribut gekennzeichnet sind (das Attribut gilt für alle Methoden des Typs).

• Get-Eigenschaftenaccessoren

• Operatoren (statische Methoden, deren Namen mit "op" beginnen und einen oder zwei Parameter und einen nicht ungültigen Rückgabetyp aufweisen).

• Jede Methode, deren vollqualifizierter Name mit "System.Diagnostics.Contracts.Contract", "System.String", "System.IO.Path" oder "System.Type" beginnt.

• Jeder aufgerufene Delegat, vorausgesetzt, dass der Delegattyp selbst mit PureAttribute attributiert ist. Die Delegattypen System.Predicate<T> und System.Comparison<T> gelten als rein.

Sichtbarkeit

Alle in einem Vertrag genannten Mitglieder müssen mindestens so sichtbar sein wie die Methode, in der sie angezeigt werden. Beispielsweise kann ein privates Feld nicht in einer Voraussetzung für eine öffentliche Methode erwähnt werden; Clients können einen solchen Vertrag nicht überprüfen, bevor sie die Methode aufrufen. Wenn das Feld jedoch mit dem ContractPublicPropertyNameAttributeFeld markiert ist, ist es von diesen Regeln ausgenommen.

Beispiel

Das folgende Beispiel zeigt die Verwendung von Codeverträgen.

#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