Codeverträge

Artikel
08/10/2011

Codeverträge bieten eine Möglichkeit, Vorbedingungen, Nachbedingungen und Objektinvarianten im Code festzulegen. Vorbedingungen sind Anforderungen, die beim Eingeben einer Methode oder Eigenschaft erfüllt werden müssen. Nachbedingungen beschreiben Erwartungen zu dem Zeitpunkt, zu dem die Methode oder der Eigenschaftencode beendet wird. Objektinvariante Elemente beschreiben den erwarteten Zustand für eine Klasse, die in einem einwandfreien Zustand ist.

Codeverträge enthalten Klassen zum Markieren des Codes, eine statische Analyse für die Kompilierzeitanalyse und eine Laufzeitanalyse. Die Klassen für Codeverträge befinden sich im System.Diagnostics.Contracts-Namespace.

Codeverträge bieten folgende Vorteile:

Verbessertes Testen: Codeverträge ermöglichen statische Vertragsüberprüfung, Laufzeitüberprüfung und Dokumentationsgenerierung.
Automatische Testtools: Sie können mithilfe von Codeverträgen aussagekräftigere Komponententests generieren, indem bedeutungslose Testargumente, die keine Vorbedingungen erfüllen, herausgefiltert werden.
Statische Überprüfung: Mit der statischen Prüfung kann bestimmt werden, ob Vertragsverletzungen vorliegen, ohne das Programm auszuführen. Es wird nach impliziten Verträgen, z. B. NULL-Dereferenzierungen und Arraygrenzen, sowie nach expliziten Verträgen gesucht.
Referenzdokumentation: Der Dokumentations-Generator erweitert vorhandene XML-Dokumentationsdateien mit Vertragsinformationen. Es gibt auch Stylesheets, die mit Sandcastle verwendet werden können, damit die generierten Dokumentationsseiten Vertragsabschnitte enthalten.

Alle .NET Framework-Sprachen können umgehend Verträge nutzen; es muss kein spezieller Parser oder Compiler geschrieben werden. Ein Visual Studio-Add-In ermöglicht die Angabe der Ebene der auszuführenden Codevertragsanalyse. Durch die Analysen kann überprüft werden, ob die Verträge wohlgeformt sind (Typüberprüfung und Namensauflösung) und ob eine kompilierte Form der Verträge im Microsoft Intermediate Language (MSIL)-Format erzeugt werden kann. Die Erstellung von Verträgen in Visual Studio ermöglicht die Nutzung der vom Tool bereitgestellten standardmäßigen IntelliSense-Funktionen.

Die meisten Methoden in der Vertragsklasse werden bedingt kompiliert; das heißt, der Compiler gibt nur dann Aufrufe dieser Methoden aus, wenn mithilfe der #define-Direktive ein besonderes Symbol definiert wird (CONTRACTS FULL). CONTRACTS FULL ermöglicht das Schreiben von Verträgen in den Code ohne Verwendung von #ifdef-Direktiven. Sie können unterschiedliche Builds erzeugen, von denen einige Verträge besitzen, andere hingegen nicht.

Tools und detaillierte Anweisungen für die Verwendung von Codeverträgen finden Sie unter Code Contracts auf der Website von MSDN DevLabs.

Vorbedingungen

Sie können Vorbedingungen mit der Contract.Requires-Methode ausdrücken. Vorbedingungen geben den Zustand bei Aufruf einer Methode an. Sie dienen im Allgemeinen zur Angabe von gültigen Parameterwerten. Auf alle Member, die in Vorbedingungen erwähnt werden, muss mindestens als die Methode selbst zugegriffen werden können. Andernfalls wird die Vorbedingung möglicherweise nicht von allen Aufrufern einer Methode verstanden. Die Bedingung darf keine zusätzlichen Auswirkungen haben. Das Laufzeitverhalten fehlerhafter Vorbedingungen wird durch die Laufzeitanalyse bestimmt.

Die folgende Vorbedingung drückt z. B. aus, dass der Parameter x nicht NULL sein muss.

Contract.Requires( x != null );

Wenn im Code eine bestimmte Ausnahme bei einem Fehler einer Vorbedingung ausgelöst werden muss, können Sie die generische Überladung von Requires folgendermaßen verwenden.

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

Ältere Requires-Anweisungen

Der Großteil des Codes enthält einige Parametervalidierungsfunktionen in Form des if-then-throw-Codes. Die Vertragstools erkennen diese Anweisungen in den folgenden Fällen als Vorbedingungen:

Die Anweisungen werden vor beliebigen anderen Anweisungen in einer Methode angezeigt.
Auf den vollständigen Satz solcher Anweisungen folgt ein expliziter Contract-Methodenaufruf, z. B. ein Aufruf der folgenden Methode: Requires, Ensures, EnsuresOnThrow oder EndContractBlock.

Wenn if-then-throw in diesem Formular angezeigt werden, werden sie von den Tools als ältere requires-Anweisungen erkannt. Wenn keine anderen Verträge auf die 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 vorangehenden Test eine negierte Vorbedingung ist. (Die tatsächliche Vorbedingung wäre x != null.) Eine negierte Vorbedingung unterliegt starken Einschränkungen: Sie muss entsprechend dem vorherigen Beispiel geschrieben werden; das heißt, sie sollte keine else-Klauseln enthalten, und der Text der then-Klausel muss eine einzelne throw-Anweisung sein. Der if-Test unterliegt gleichermaßen Klarheits- als auch Sichtbarkeitsregeln (siehe Verwendungsrichtlinien), doch der throw-Ausdruck unterliegt nur Klarheitsregeln. Der Typ der ausgelösten Ausnahme, muss als die Methode sichtbar sein, in der der Vertrag auftritt.

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 fehlerhafter Nachbedingungen wird durch die Laufzeitanalyse bestimmt.

Im Gegensatz zu Vorbedingungen verweisen Nachbedingungen möglicherweise mit geringerer Sichtbarkeit auf Member. 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, doch dies beeinträchtigt nicht die Fähigkeit des Clients, die Methode ordnungsgemäß zu verwenden.

Standardmäßige Nachbedingungen

Sie können standardmäßige Nachbedingungen mithilfe der Ensures-Methode ausdrücken. Nachbedingungen drücken eine Bedingung aus, die bei normalem Beenden der Methode true sein muss.

Contract.Ensures( this .F > 0 );

Ausnahmenachbedingungen

Ausnahmenachbedingungen sind Nachbedingungen, die true sein sollten, wenn eine bestimmte Ausnahme von einer Methode ausgelöst wird. Sie können diese Nachbedingungen mit der Contract.EnsuresOnThrow-Methode angeben (siehe folgendes Beispiel).

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

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

Es gibt einige Ausnahmetypen, die in einer Ausnahmenachbedingung nur unter Schwierigkeiten zu verwenden sind. Zum Beispiel erfordert die Verwendung des Exception-Typs für T, dass die Bedingung durch die Methode unabhängig vom Typ der ausgelösten Ausnahme gewährleistet wird, auch wenn es sich um einen Stapelüberlauf oder eine andere nicht kontrollierbare Ausnahme handelt. Sie sollten Ausnahmenachbedingungen nur für bestimmte Ausnahmen verwenden, die beim Aufruf eines Members ausgelöst werden könnten, z. B., wenn ein InvalidTimeZoneException-Objekt für einen TimeZoneInfo-Methodenaufruf ausgelöst wird.

Besondere Nachbedingungen

Die folgenden Methoden werden möglicherweise nur innerhalb von Nachbedingungen verwendet:

Sie können mit dem Ausdruck Contract. Result<T>(), in dem T vom Rückgabetyp der Methode ersetzt wird, auf Methodenrückgabewerte in Postkonditionen verweisen. Wenn der Compiler den Typ nicht ableiten kann, muss er explizit angegeben werden. Der C#-Compiler kann z. B. keine Typen für Methoden ableiten, die keine Argumente akzeptieren. Daher ist die folgende Nachbedingung erforderlich: Contract.Ensures(0 < Contract.Result<int>())-Methoden mit dem Rückgabetyp void können in ihren Postkonditionen nicht auf Contract. Result<T>() verweisen.

Ein prestate-Wert in einer Nachbedingung verweist auf den Wert eines Ausdrucks am Beginn einer Methode oder einer Eigenschaft. Für den Wert wird der Ausdruck Contract.OldValue<T>(e) verwendet, wobei T der Typ von e ist. Sie können das generische Typargument auslassen, wenn der Compiler den Typ ableiten kann. (Zum Beispiel leitet der C#-Compiler immer den Typ ab, da er ein Argument erhält.) Es gibt mehrere Einschränkungen bezüglich dessen, was in e und den Kontexten auftreten kann, in denen möglicherweise ein alter Ausdruck angezeigt wird. Ein alter Ausdruck darf keinen anderen alten Ausdruck enthalten. Am wichtigsten ist, dass ein alter Ausdruck auf einen Wert verweist, der im Vorbedingungszustand der Methode vorhanden war. Anders ausgedrückt, es muss sich um einen Ausdruck handeln, der ausgewertet werden kann, solange die Vorbedingung der Methode true ist. Hier sind mehrere Instanzen dieser Regel.

Der Wert muss im Vorbedingungszustand der Methode vorhanden sein. Um auf ein Feld in einem Objekt zu verweisen, muss durch die Vorbedingungen gewährleistet sein, 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 nicht auf out-Parameter in einem alten Ausdruck verweisen.
Ein alter Ausdruck kann nicht von der gebundenen Variable 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-Aufruf oder Exists-Aufruf verweisen, sofern er nicht als Indexer oder Argument für einen Methodenaufruf verwendet wird:
```
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 Text eines anonymen Delegaten auftreten, wenn der Wert des alten Ausdrucks von einem der Parameter des anonymen Delegaten abhängt, sofern der anonyme Delegat kein Argument für die ForAll-Methode oder die Exists-Methode ist:
```
Method( ... (T t) => Contract.OldValue(... t ...) ... ); // ERROR
```

Out-Parameter stellen ein Problem dar, da Verträge vor dem Text der Methode angezeigt werden, und die meisten Compiler lassen keine Verweise auf out-Parameter in Nachbedingungen zu. Zur Lösung des Problems steht in der Contract-Klasse die ValueAtReturn<T>-Methode zur Verfügung. Sie lässt eine Nachbedingung auf Grundlage eines out-Parameters zu.

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

Ebenso wie mit der OldValue<T>-Methode können Sie den generischen Typparameter weglassen, wenn der Compiler den Typ ableiten kann. Der Vertrags-Rewriter ersetzt den Methodenaufruf durch den Wert des out-Parameters. Die ValueAtReturn<T>-Methode wird möglicherweise nur in Nachbedingungen angezeigt. Das Argument für die Methode muss ein out-Parameter oder ein Feld eines strukturbezogenen out-Parameters sein. Die letztere Methode ist ebenfalls hilfreich, wenn auf Felder in der Nachbedingung eines Strukturkonstruktors verwiesen wird.

Hinweis
Derzeit wird von den Vertragsanalysetools nicht überprüft, ob out-Parameter ordnungsgemäß initialisiert werden, und deren Nennung in der Nachbedingung wird nicht beachtet.Wenn im vorherigen Beispiel in der Zeile nach dem Vertrag der Wert von x verwendet worden wäre, anstatt der Zeile eine ganze Zahl zuzuweisen, würde ein Compiler nicht den entsprechenden Fehler ausgeben.Allerdings gibt der Compiler in einem Build, in dem das CONTRACTS FULL-Präprozessorsymbol nicht definiert ist (z. B.ein Releasebuild), einen Fehler aus.

Derzeit wird von den Vertragsanalysetools nicht überprüft, ob out-Parameter ordnungsgemäß initialisiert werden, und deren Nennung in der Nachbedingung wird nicht beachtet.Wenn im vorherigen Beispiel in der Zeile nach dem Vertrag der Wert von x verwendet worden wäre, anstatt der Zeile eine ganze Zahl zuzuweisen, würde ein Compiler nicht den entsprechenden Fehler ausgeben.Allerdings gibt der Compiler in einem Build, in dem das CONTRACTS FULL-Präprozessorsymbol nicht definiert ist (z. B.ein Releasebuild), einen Fehler aus.

Invarianten

Objektinvarianten sind Bedingungen, die für jede Instanz einer Klasse den Wert "true" ergeben sollten, wenn das Objekt für einen Client sichtbar ist. Sie drücken die Bedingungen aus, unter denen das Objekt als korrekt eingestuft wird.

Die invarianten Methoden werden identifiziert, indem sie mit dem ContractInvariantMethodAttribute-Attribut markiert werden. Die invarianten Methoden dürfen keinen Code enthalten, mit Ausnahme einer Sequenz von Aufrufen der Invariant-Methode, von denen jeder eine einzelne Invariante angibt (siehe folgendes Beispiel).

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

Invariante Elemente werden bedingt durch das CONTRACTS FULL- Präprozessorsymbol definiert. Während der Laufzeitüberprüfung werden invariante Elemente am Ende jeder öffentlichen Methode überprüft. Wenn ein invariantes Element eine öffentliche Methode in der gleichen Klasse erwähnt, wird die Überprüfung invarianter Elemente, die normalerweise am Ende dieser öffentlichen Methode stattfindet, deaktiviert. Stattdessen wird die Überprüfung nur am Ende des äußersten Methodenaufrufs dieser Klasse ausgeführt. Dies geschieht auch, wenn die Klasse wegen eines Anrufs einer Methode in einer anderen Klasse erneut eingegeben wird. Invariante Elemente werden nicht auf Objektfinalizer oder Methoden überprüft, mit denen die Dispose-Methode implementiert wird.

Verwendungsrichtlinien

Verträge – Reihenfolge

In der folgenden Tabelle wird die Reihenfolge der Elemente angezeigt, die beim Schreiben von Methodenverträgen verwendet werden sollen.

If-then-throw statements	Abwärtskompatible öffentliche Vorbedingungen
Requires	Alle öffentlichen Vorbedingungen.
Ensures	Alle öffentlichen (normalen) Nachbedingungen.
EnsuresOnThrow	Alle öffentlichen Ausnahmenachbedingungen.
Ensures	Alle privaten/internen (normalen) Nachbedingungen.
EnsuresOnThrow	Alle privaten/internen Ausnahmenachbedingungen.
EndContractBlock	Bei Verwendung der if-then-throw-Formatvorbedingungen ohne andere Verträge rufen Sie EndContractBlock auf, um anzugeben, dass es sich bei allen um frühere Bedingungen handelt, wenn die Prüfungen Vorbedingungen sind.

Reinheit

Alle Methoden, die in einem Vertrag aufgerufen werden, müssen rein sein; das heißt, es darf kein bereits vorhandener Zustand aktualisiert werden. Mit einer reinen Methode dürfen Objekte geändert werden, die nach Eintragung in die reine Methode erstellt wurden.

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

Methoden, die mit PureAttribute-Objekt markiert sind.
Typen, die mit dem PureAttribute-Objekt markiert sind (das Attribut gilt für alle Methoden des Typs).
Eigenschaft – get-Accessoren
Operatoren (statische Methoden, deren Namen mit "op" beginnen, die einen oder zwei Parameter und einen nicht ungültigen Rückgabetyp besitzen).
Eine beliebige Methode, deren vollqualifizierter Name mit "System.Diagnostics.Contracts.Contract", "System.String", "System.IO.Path" oder "System.Type" beginnt.
Ein beliebiger aufgerufener Delegat, vorausgesetzt, dass dem Delegattyp selbst das PureAttribute-Objekt zugewiesen wird. Die Delegattypen System.Predicate<T> und System.Comparison<T> werden als rein eingestuft.

Sichtbarkeit

Alle in einem Vertrag erwähnten Member müssen mindestens ebenso sichtbar sein wie die Methode, in der sie angezeigt werden. Ein privates Feld kann z. B. nicht in einer Vorbedingung für eine öffentliche Methode erwähnt werden; Clients können keinen derartigen Vertrag überprüfen, bevor sie die Methode aufrufen. Wenn das Feld jedoch mit dem ContractPublicPropertyNameAttribute-Objekt markiert wird, ist es von diesen Regeln befreit.

Beispiel

Im folgenden Beispiel wird die Verwendung von Codeverträgen veranschaulicht.

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