Kontrakty kódu (.NET Framework)

Kontrakty kódu poskytují způsob, jak určit předpoklady, postconditions a invarianty objektů v kódu rozhraní .NET Framework. Předpoklady jsou požadavky, které musí být splněny při zadávání metody nebo vlastnosti. Postconditions popisuje očekávání v době, kdy metoda nebo kód vlastnosti ukončí. Invarianty objektů popisují očekávaný stav třídy, která je v dobrém stavu.

Kontrakty kódu zahrnují třídy pro označení kódu, statický analyzátor pro analýzu času kompilace a analyzátor modulu runtime. Třídy kontraktů kódu najdete v System.Diagnostics.Contracts oboru názvů.

Mezi výhody kontraktů kódu patří:

• Vylepšené testování: Kontrakty kódu poskytují statické ověřování kontraktů, kontrolu za běhu a generování dokumentace.

• Nástroje pro automatické testování: Kontrakty kódu můžete použít k vygenerování smysluplnějších testů jednotek vyfiltrováním bezvýznamných testovacích argumentů, které nesplňují předpoklady.

• Statické ověření: Statická kontrola může rozhodnout, jestli nedošlo k porušení smlouvy bez spuštění programu. Kontroluje implicitní kontrakty, například nulové dereference a hranice polí a explicitní kontrakty.

• Referenční dokumentace: Generátor dokumentace rozšiřuje existující soubory dokumentace XML informacemi o kontraktech. K dispozici jsou také šablony stylů, které lze použít s Sandcastle , aby vygenerované stránky dokumentace měly oddíly kontraktů.

Všechny jazyky rozhraní .NET Framework mohou okamžitě využívat kontrakty; Nemusíte psát speciální analyzátor ani kompilátor. Doplněk sady Visual Studio umožňuje určit úroveň analýzy kontraktů kódu, která se má provést. Analyzátory můžou potvrdit, že kontrakty jsou správně vytvořené (kontrola typů a překlad názvů) a mohou vytvořit kompilovanou formu kontraktů ve formátu CIL (Common Intermediate Language). Vytváření kontraktů v sadě Visual Studio umožňuje využívat standardní technologii IntelliSense poskytovanou nástrojem.

Většina metod ve třídě kontraktu je podmíněně kompilována; to znamená, že kompilátor generuje volání těchto metod pouze v případě, že definujete speciální symbol, CONTRACTS_FULL, pomocí direktivy #define . CONTRACTS_FULL umožňuje psát kontrakty v kódu bez použití #ifdef direktiv. Můžete vytvářet různá sestavení, některá s kontrakty a některá bez nich.

Nástroje a podrobné pokyny pro použití kontraktů kódu najdete v tématu Kontrakty kódu na webu Visual Studio Marketplace.

Předpoklady

Pomocí metody můžete vyjádřit předběžné podmínky Contract.Requires . Předpoklady určují stav při vyvolání metody. Obvykle se používají k určení platných hodnot parametrů. Všichni členové, kteří jsou zmíněni v předběžných předpokladech, musí být alespoň tak přístupní jako samotná metoda; jinak nemusí být předběžná podmínka srozumitelná pro všechny volající metody. Podmínka nesmí mít žádné vedlejší účinky. Chování neúspěšných předpokladů za běhu je určeno analyzátorem modulu runtime.

Následující předběžná podmínka například vyjadřuje, že parametr x musí být nenulový.

Contract.Requires(x != null);

Pokud váš kód musí vyvolat konkrétní výjimku při selhání předběžné podmínky, můžete použít obecné přetížení Requires následujícím způsobem.

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

Starší verze vyžaduje příkazy

Většina kódu obsahuje ověření parametru if--thenthrow ve formě kódu. Smluvní nástroje tyto příkazy rozpoznávají jako předpoklady v následujících případech:

• Příkazy se zobrazí před jinými příkazy v metodě.

• Za celou sadou takových příkazů následuje explicitní Contract volání metody, například volání Requires, Ensures, EnsuresOnThrownebo EndContractBlock metody.

Když if--thenthrow se příkazy zobrazí v tomto formuláři, nástroje je rozpoznávají jako starší requires příkazy. Pokud žádné jiné kontrakty nedodržují if--thenthrow sekvenci, ukončete kód metodou.Contract.EndContractBlock

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

Všimněte si, že podmínka v předchozím testu je negovanou podmínkou. (Skutečná předběžná podmínka by byla x != null.) Předběžná podmínka je vysoce omezená: Musí být napsána, jak je uvedeno v předchozím příkladu; to znamená, že by neměla obsahovat žádné else klauzule a tělo then klauzule musí být jediným throw příkazem. Test if podléhá čistotě i pravidlům viditelnosti (viz Pokyny k používání), ale throw výraz podléhá pouze pravidlům čistoty. Typ vyvolané výjimky však musí být viditelný jako metoda, ve které dochází ke kontraktu.

Postconditions

Postconditions jsou kontrakty pro stav metody při ukončení. Postcondition se kontroluje těsně před ukončením metody. Chování neúspěšných postconditions je určeno analyzátorem modulu runtime.

Na rozdíl od předpokladů mohou postconditions odkazovat na členy s nižší viditelností. Klient nemusí být schopen pochopit nebo využít některé informace vyjádřené postcondition pomocí privátního stavu, ale to nemá vliv na schopnost klienta správně používat metodu.

Standardní postconditions

Standardní postconditions můžete vyjádřit pomocí Ensures metody. Postconditions vyjadřuje podmínku, která musí být true při normálním ukončení metody.

Contract.Ensures(this.F > 0);

Výjimečné postconditions

Mimořádné postconditions jsou postconditions, které by měly být true , když je konkrétní výjimka vyvolán metodou. Tyto postconditions můžete zadat pomocí Contract.EnsuresOnThrow metody, jak ukazuje následující příklad.

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

Argument je podmínka, která musí být true vždy, když je vyvolán výjimka, která je podtyp vyvolán T .

Existují některé typy výjimek, které jsou obtížné použít v mimořádné postcondition. Například použití typu Exception pro T vyžaduje, aby metoda zaručit podmínku bez ohledu na typ výjimky, která je vyvolán, i když se jedná o přetečení zásobníku nebo jinou výjimku nemožné-to-control. Měli byste použít výjimečné postconditions pouze pro konkrétní výjimky, které mohou být vyvolány při volání člena, například při InvalidTimeZoneException vyvolání TimeZoneInfo volání metody.

Speciální postconditions

Následující metody lze použít pouze v rámci postconditions:

• Můžete odkazovat na metody návratové hodnoty v postconditions pomocí výrazu Contract.Result<T>(), kde T je nahrazen návratovým typem metody. Pokud kompilátor nemůže typ odvodit, musíte ho explicitně zadat. Kompilátor jazyka C# například nemůže odvodit typy pro metody, které nepřebírají žádné argumenty, takže vyžaduje následující postcondition: Contract.Ensures(0 <Contract.Result<int>()) Metody s návratovým typem void nemohou odkazovat Contract.Result<T>() v jejich postconditions.

• Hodnota předběžného stavu v postcondition odkazuje na hodnotu výrazu na začátku metody nebo vlastnosti. Používá výraz Contract.OldValue<T>(e), kde T je typ e. Argument obecného typu můžete vynechat vždy, když kompilátor dokáže odvodit jeho typ. (Kompilátor jazyka C# například vždy odvodí typ, protože přebírá argument.) Existuje několik omezení, ke kterým může dojít e , a kontexty, ve kterých se může zobrazit starý výraz. Starý výraz nemůže obsahovat jiný starý výraz. Nejdůležitější je, že starý výraz musí odkazovat na hodnotu, která existovala v předběžném stavu metody. Jinými slovy, musí se jednat o výraz, který lze vyhodnotit, pokud je truepředběžná podmínka metody . Tady je několik instancí tohoto pravidla.

  • Hodnota musí existovat v předběžném stavu metody. Aby bylo možné odkazovat na pole objektu, musí předpoklady zaručit, že objekt je vždy nenulový.

  • Ve starém výrazu nelze odkazovat na návratovou hodnotu metody:

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

  • Ve starém výrazu nelze odkazovat na out parametry.

  • Starý výraz nemůže záviset na vázané proměnné kvantifikátoru, pokud rozsah kvantifikátoru závisí na návratové hodnotě metody:

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

  • Starý výraz nemůže odkazovat na parametr anonymního delegáta v objektu ForAll nebo Exists volání, pokud se nepoužívá jako indexer nebo argument volání metody:

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

  • Starý výraz nemůže nastat v těle anonymního delegáta, pokud hodnota starého výrazu závisí na některé z parametrů anonymního delegáta, pokud anonymní delegát není argumentem pro metodu nebo Exists metoduForAll:

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

  • Out parametry představují problém, protože kontrakty se zobrazují před tělem metody a většina kompilátorů neumožňuje odkazy na out parametry v postconditions. K vyřešení tohoto problému Contract třída poskytuje metodu ValueAtReturn , která umožňuje postcondition na základě parametru out .

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

    Stejně jako u OldValue metody můžete vynechat parametr obecného typu vždy, když kompilátor dokáže odvodit jeho typ. Autor kontraktu nahrazuje volání metody hodnotou parametru out . Metoda ValueAtReturn se může objevit pouze v postconditions. Argumentem metody musí být out parametr nebo pole parametru struktury out . Druhý je také užitečný při odkazování na pole v postcondition konstruktoru struktury.

    Poznámka:

    Nástroje pro analýzu kontraktů kódu v současné době nekontrolují, jestli out jsou parametry inicializovány správně, a ignorují jejich zmínky v postcondition. V předchozím příkladu by tedy kompilátor nevydával správnou chybu, pokud řádek za kontraktem použil hodnotu x namísto přiřazení celého čísla. V sestavení, kde není definován symbol preprocesoru CONTRACTS_FULL (například sestavení verze), kompilátor vydá chybu.

Invariants

Invarianty objektů jsou podmínky, které by měly být splněny pro každou instanci třídy vždy, když je tento objekt viditelný pro klienta. Vyjadřují podmínky, za kterých je objekt považován za správný.

Invariantní metody jsou identifikovány tím, že jsou označeny atributem ContractInvariantMethodAttribute . Invariantní metody nesmí obsahovat žádný kód s výjimkou posloupnosti volání Invariant metody, z nichž každá určuje jednotlivou invariantní metodu, jak je znázorněno v následujícím příkladu.

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

Invarianty jsou podmíněně definovány symbolem preprocesoru CONTRACTS_FULL. Během kontroly za běhu se invarianty kontrolují na konci každé veřejné metody. Pokud invariant zmíní veřejnou metodu ve stejné třídě, invariantní kontrola, která by se normálně stala na konci této veřejné metody, je zakázaná. Místo toho se kontrola provádí pouze na konci vnější metody volání této třídy. K tomu dochází také v případě, že je třída znovu zadána kvůli volání metody v jiné třídě. Invarianty nejsou kontrolovány pro finalizátor objektů a implementaci IDisposable.Dispose .

Pokyny k používání

Řazení kontraktů

Následující tabulka ukazuje pořadí prvků, které byste měli použít při psaní kontraktů metod.

Čistotu

Všechny metody volané v rámci kontraktu musí být čisté; to znamená, že nesmí aktualizovat žádný existující stav. Čistá metoda může upravovat objekty, které byly vytvořeny po zadání do čisté metody.

Nástroje kontraktu kódu v současné době předpokládají, že následující prvky kódu jsou čisté:

• Metody, které jsou označeny značkou PureAttribute.

• Typy, které jsou označené PureAttribute symbolem (atribut platí pro všechny metody typu).

• Vlastnost get accessors.

• Operátory (statické metody, jejichž názvy začínají na "op" a které mají jeden nebo dva parametry a návratový typ bez void).

• Jakákoli metoda, jejíž plně kvalifikovaný název začíná na "System.Diagnostics.Contracts.Contract", "System.String", "System.IO.Path" nebo "System.Type".

• Jakýkoli vyvolaný delegát za předpokladu, že samotný typ delegáta je přiřazen .PureAttribute Typy delegátů System.Predicate<T> a System.Comparison<T> jsou považovány za čisté.

Viditelnost

Všichni členové zmínění ve smlouvě musí být alespoň tak viditelné jako metoda, ve které se zobrazují. Soukromé pole například nelze zmínit v předběžném předpokladu pro veřejnou metodu; klienti nemohou takovou smlouvu před voláním metody ověřit. Pokud je však pole označené symbolem ContractPublicPropertyNameAttribute, je z těchto pravidel vyloučeno.

Příklad

Následující příklad ukazuje použití kontraktů kódu.

#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