Kontrakty kodu (.NET Framework)

  • Artykuł

Kontrakty kodu umożliwiają określenie warunków wstępnych, pokondycji i niezmiennych obiektów w kodzie programu .NET Framework. Warunki wstępne są wymaganiami, które muszą zostać spełnione podczas wprowadzania metody lub właściwości. Postconditions opisują oczekiwania w czasie zakończenia metody lub kodu właściwości. Niezmienne obiekty opisują oczekiwany stan klasy, która jest w dobrym stanie.

Uwaga

Kontrakty kodu nie są obsługiwane na platformie .NET 5+ (w tym w wersjach platformy .NET Core). Zamiast tego rozważ użycie typów odwołań dopuszczanych wartości null.

Kontrakty kodu obejmują klasy oznaczania kodu, analizatora statycznego do analizy czasu kompilacji i analizatora środowiska uruchomieniowego. Klasy kontraktów kodu można znaleźć w System.Diagnostics.Contracts przestrzeni nazw.

Zalety kontraktów kodu obejmują następujące elementy:

  • Ulepszone testowanie: Kontrakty kodu zapewniają statyczną weryfikację kontraktu, sprawdzanie środowiska uruchomieniowego i generowanie dokumentacji.

  • Narzędzia do testowania automatycznego: możesz użyć kontraktów kodu, aby wygenerować bardziej znaczące testy jednostkowe, filtrując bezsensowne argumenty testów, które nie spełniają warunków wstępnych.

  • Weryfikacja statyczna: statyczny moduł sprawdzania może zdecydować, czy istnieją jakiekolwiek naruszenia umowy bez uruchamiania programu. Sprawdza ona kontrakty niejawne, takie jak wyłudywanie wartości null i granice tablicy oraz jawne kontrakty.

  • Dokumentacja referencyjna: Generator dokumentacji rozszerza istniejące pliki dokumentacji XML o informacje o umowie. Istnieją również arkusze stylów, których można używać z platformą Sandcastle , aby strony wygenerowanej dokumentacji miały sekcje kontraktu.

Wszystkie języki programu .NET Framework mogą natychmiast korzystać z kontraktów; nie trzeba pisać specjalnego analizatora ani kompilatora. Dodatek programu Visual Studio umożliwia określenie poziomu analizy kontraktu kodu do wykonania. Analizatory mogą potwierdzić, że kontrakty są prawidłowo sformułowane (sprawdzanie typów i rozpoznawanie nazw) i mogą utworzyć skompilowany formularz kontraktów w formacie wspólnego języka pośredniego (CIL). Tworzenie kontraktów w programie Visual Studio umożliwia korzystanie ze standardowej funkcji IntelliSense udostępnianej przez narzędzie.

Większość metod w klasie kontraktu jest kompilowana warunkowo; oznacza to, że kompilator emituje wywołania do tych metod tylko wtedy, gdy definiujesz specjalny symbol, CONTRACTS_FULL, przy użyciu #define dyrektywy . CONTRACTS_FULL umożliwia pisanie kontraktów w kodzie bez używania #ifdef dyrektyw. Można tworzyć różne kompilacje, niektóre z kontraktami i niektóre bez.

Aby zapoznać się z narzędziami i szczegółowymi instrukcjami dotyczącymi używania kontraktów kodu, zobacz Code Contracts (Kontrakty kodu) w witrynie marketplace programu Visual Studio.

Warunki wstępne

Warunki wstępne można wyrazić przy użyciu Contract.Requires metody . Warunek wstępny określa stan po wywołaniu metody. Są one zwykle używane do określania prawidłowych wartości parametrów. Wszystkie elementy członkowskie wymienione w warunkach wstępnych muszą być co najmniej tak dostępne jak sama metoda; w przeciwnym razie warunek wstępny może nie być rozumiany przez wszystkie wywołujące metodę. Warunek nie może mieć skutków ubocznych. Zachowanie w czasie wykonywania nieudanych warunków wstępnych jest określane przez analizator środowiska uruchomieniowego.

Na przykład poniższy warunek wstępny wyraża, że parametr x musi mieć wartość inną niż null.

Contract.Requires(x != null);

Jeśli kod musi zgłosić określony wyjątek w przypadku niepowodzenia warunku wstępnego, możesz użyć ogólnego przeciążenia Requires w następujący sposób.

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

Starsza wersja wymaga instrukcji

Większość kodu zawiera weryfikację parametrów if--thenthrow w postaci kodu. Narzędzia kontraktowe uznają te instrukcje za warunek wstępny w następujących przypadkach:

Gdy if--thenthrow instrukcje są wyświetlane w tym formularzu, narzędzia rozpoznają je jako starsze requires instrukcje. Jeśli żadne inne kontrakty nie są zgodne z sekwencjąif--thenthrow, zakończ kod metodą .Contract.EndContractBlock

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

Należy pamiętać, że warunek w poprzednim teście jest negowanym warunkiem wstępnym. (Rzeczywistym warunkiem wstępnym byłoby x != null.) Negowany warunek wstępny jest bardzo ograniczony: musi być napisany, jak pokazano w poprzednim przykładzie; oznacza to, że nie powinien zawierać else żadnych klauzul, a treść klauzuli then musi być pojedynczą throw instrukcją. Test if podlega zarówno regułom czystości, jak i widoczności (zobacz Wytyczne dotyczące użycia), ale throw wyrażenie podlega tylko regułom czystości. Jednak typ zgłaszanego wyjątku musi być tak widoczny, jak metoda, w której występuje kontrakt.

Postconditions

Terminy końcowe to kontrakty stanu metody po zakończeniu. Przed zamknięciem metody sprawdzana jest wartość postcondition. Zachowanie czasu wykonywania po awarii jest określane przez analizator środowiska uruchomieniowego.

W przeciwieństwie do warunków wstępnych, postconditions mogą odwoływać się do elementów członkowskich o mniejszej widoczności. Klient może nie być w stanie zrozumieć lub użyć niektórych informacji wyrażonych po awarii przy użyciu stanu prywatnego, ale nie ma to wpływu na zdolność klienta do prawidłowego używania metody.

Standardowe wersje postcondition

Standardowe postconditions można wyrazić przy użyciu Ensures metody . Postconditions wyrażają warunek, który musi znajdować się true po normalnym zakończeniu metody.

Contract.Ensures(this.F > 0);

Wyjątkowe postconditions

Wyjątkowe postconditions są postconditions, które powinny być true , gdy określony wyjątek jest zgłaszany przez metodę. Te wartości końcowe można określić przy użyciu Contract.EnsuresOnThrow metody , jak pokazano w poniższym przykładzie.

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

Argument jest warunkiem, który musi być true zawsze, gdy jest zgłaszany wyjątek, który jest podtypem T .

Istnieją pewne typy wyjątków, które są trudne do użycia w wyjątkowej pośmiertnie. Na przykład użycie typu Exception dla T parametru wymaga metody zagwarantowania warunku niezależnie od typu wyjątku, który jest zgłaszany, nawet jeśli jest to przepełnienie stosu lub inny niemożliwy do sterowania wyjątek. Należy użyć wyjątkowych pokondycji tylko w przypadku określonych wyjątków, które mogą być zgłaszane, gdy element członkowski jest wywoływany, na przykład, gdy InvalidTimeZoneException element jest zgłaszany dla wywołania TimeZoneInfo metody.

Specjalne postconditions

Następujące metody mogą być używane tylko w ramach pokondycji:

  • Możesz odwołać się do zwracanych wartości metody w wyrażeniach postcondition przy użyciu wyrażenia Contract.Result<T>(), gdzie T jest zastępowany przez zwracany typ metody. Jeśli kompilator nie może wywnioskować typu, musisz jawnie go podać. Na przykład kompilator języka C# nie może wywnioskować typów metod, które nie przyjmują żadnych argumentów, dlatego wymaga następującego postkondycji: Contract.Ensures(0 <Contract.Result<int>()) Metody z typem void zwrotnym nie mogą odwoływać się do Contract.Result<T>() w swoich postconditions.

  • Wartość prestate w pokondycji odnosi się do wartości wyrażenia na początku metody lub właściwości. Używa wyrażenia Contract.OldValue<T>(e), gdzie T jest typem e. Można pominąć argument typu ogólnego, gdy kompilator może wywnioskować jego typ. (Na przykład kompilator języka C# zawsze wywnioskuje typ, ponieważ przyjmuje argument). Istnieje kilka ograniczeń dotyczących tego, co może wystąpić w e i kontekstach, w których może pojawić się stare wyrażenie. Stare wyrażenie nie może zawierać innego starego wyrażenia. Co najważniejsze, stare wyrażenie musi odwoływać się do wartości, która istniała w stanie warunków wstępnych metody. Innymi słowy, musi to być wyrażenie, które można ocenić tak długo, jak warunek wstępny metody to true. Oto kilka wystąpień tej reguły.

    • Wartość musi istnieć w stanie warunku wstępnego metody. Aby odwołać się do pola w obiekcie, warunki wstępne muszą zagwarantować, że obiekt jest zawsze inny niż null.

    • Nie można odwołać się do wartości zwracanej metody w starym wyrażeniu:

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

    • Nie można odwoływać się do out parametrów w starym wyrażeniu.

    • Stare wyrażenie nie może zależeć od zmiennej powiązanej kwantyfikatora, jeśli zakres kwantyfikatora zależy od wartości zwracanej metody:

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

    • Stare wyrażenie nie może odwoływać się do parametru delegata anonimowego w wywołaniu ForAll lub Exists , chyba że jest ono używane jako indeksator lub argument do wywołania metody:

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

    • Stare wyrażenie nie może wystąpić w treści delegata anonimowego, jeśli wartość starego wyrażenia zależy od któregokolwiek z parametrów delegata anonimowego, chyba że pełnomocnik anonimowy jest argumentem ForAll metody or Exists :

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

    • Out parametry stanowią problem, ponieważ kontrakty pojawiają się przed treścią metody, a większość kompilatorów nie zezwala na odwołania do out parametrów w parametrach postcondition. Aby rozwiązać ten problem, Contract klasa udostępnia metodę ValueAtReturn , która umożliwia pokondycję na podstawie parametru out .

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

      Podobnie jak w przypadku OldValue metody, można pominąć parametr typu ogólnego za każdym razem, gdy kompilator może wywnioskować jego typ. Wymiana kontraktu zastępuje wywołanie metody wartością parametru out . Metoda może być wyświetlana ValueAtReturn tylko w postconditions. Argument metody musi być parametrem out lub polem parametru struktury out . Ten ostatni jest również przydatny podczas odwoływania się do pól po zakończeniu konstruktora struktury.

      Uwaga

      Obecnie narzędzia do analizy kontraktu kodu nie sprawdzają, czy out parametry są inicjowane prawidłowo i ignorują ich wzmiankę w powłoce. W związku z tym w poprzednim przykładzie, jeśli wiersz po kontrakcie użył wartości x zamiast przypisywać do niej liczbę całkowitą, kompilator nie wystawi poprawnego błędu. Jednak w przypadku kompilacji, w której nie zdefiniowano symbolu preprocesora CONTRACTS_FULL (np. kompilacji wydania), kompilator wystawi błąd.

Invariants

Niezmienne obiekty to warunki, które powinny być prawdziwe dla każdego wystąpienia klasy, gdy ten obiekt jest widoczny dla klienta. Wyrażają one warunki, w których obiekt jest uznawany za poprawny.

Niezmienne metody są identyfikowane przez oznaczenie za pomocą atrybutu ContractInvariantMethodAttribute . Niezmienne metody nie mogą zawierać kodu z wyjątkiem sekwencji wywołań Invariant metody, z których każda określa pojedynczą niezmienność, jak pokazano w poniższym przykładzie.

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

Zmienne są warunkowo definiowane przez symbol preprocesora CONTRACTS_FULL. Podczas sprawdzania czasu wykonywania zmienne są sprawdzane na końcu każdej metody publicznej. Jeśli niezmienna metoda wskazuje metodę publiczną w tej samej klasie, niezmienne sprawdzanie, które zwykle miało miejsce na końcu tej metody publicznej, jest wyłączone. Zamiast tego sprawdzanie odbywa się tylko na końcu najbardziej zewnętrznego wywołania metody do tej klasy. Dzieje się tak również w przypadku ponownego wprowadzenia klasy z powodu wywołania metody w innej klasie. Niezmienne nie są sprawdzane pod kątem finalizatora obiektów i implementacji IDisposable.Dispose .

Zalecenia dotyczące użytkowania

Zamawianie kontraktów

W poniższej tabeli przedstawiono kolejność elementów, których należy użyć podczas pisania kontraktów metod.

If-then-throw statements Warunki wstępne publiczne zgodne z poprzednimi wersjami
Requires Wszystkie publiczne warunki wstępne.
Ensures Wszystkie publiczne (normalne) postconditions.
EnsuresOnThrow Wszystkie publiczne wyjątkowe postconditions.
Ensures Wszystkie prywatne/wewnętrzne (normalne) pokondycji.
EnsuresOnThrow Wszystkie prywatne/wewnętrzne wyjątkowe postconditions.
EndContractBlock Jeśli używasz if--thenthrow warunków wstępnych stylu bez żadnych innych kontraktów, umieść wywołanie, aby wskazaćEndContractBlock, że wszystkie poprzednie, jeśli kontrole są warunkiem wstępnym.

Czystości

Wszystkie metody wywoływane w ramach kontraktu muszą być czyste; oznacza to, że nie mogą aktualizować żadnego istniejącego stanu. Czysta metoda może modyfikować obiekty, które zostały utworzone po wprowadzeniu do czystej metody.

Narzędzia kontraktów kodu obecnie zakładają, że następujące elementy kodu są czyste:

  • Metody oznaczone znakiem PureAttribute.

  • Typy oznaczone znakiem PureAttribute (atrybut ma zastosowanie do wszystkich metod typu).

  • Właściwość pobiera metody dostępu.

  • Operatory (metody statyczne, których nazwy zaczynają się od "op", i które mają jeden lub dwa parametry i niepusty typ zwracany).

  • Każda metoda, której w pełni kwalifikowana nazwa zaczyna się od "System.Diagnostics.Contracts.Contract", "System.String", "System.IO.Path" lub "System.Type".

  • Każdy wywoływany delegat, pod warunkiem, że sam typ delegata jest przypisywany za pomocą .PureAttribute Typy delegatów System.Predicate<T> i System.Comparison<T> są uważane za czyste.

Widoczność

Wszyscy członkowie wymienieni w umowie muszą być co najmniej tak widoczni, jak metoda, w której się pojawiają. Na przykład nie można wspomnieć o polu prywatnym w warunku wstępnym dla metody publicznej; klienci nie mogą zweryfikować takiego kontraktu przed wywołaniem metody. Jeśli jednak pole jest oznaczone znakiem ContractPublicPropertyNameAttribute, jest wykluczone z tych reguł.

Przykład

W poniższym przykładzie pokazano użycie kontraktów kodu.

#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