코드 계약(.NET Framework)

코드 계약은 .NET Framework 코드에서 사전 조건, 사후 조건 및 개체 고정을 지정하는 방법을 제공합니다. 사전 조건은 메서드 또는 속성을 입력할 때 충족해야 하는 요구 사항입니다. 사후 조건은 메서드 또는 속성 코드가 종료될 때의 기대치를 설명합니다. 개체 불변식은 클래스가 좋은 상태일 때의 예상되는 상태를 설명합니다.

코드 계약에는 코드를 표시하기 위한 클래스, 컴파일 시간 분석을 위한 정적 분석기 및 런타임 분석기가 포함됩니다. 코드 계약에 대한 클래스는 네임스페이 System.Diagnostics.Contracts 스에서 찾을 수 있습니다.

코드 계약의 이점은 다음과 같습니다.

• 향상된 테스트: 코드 계약은 정적 계약 확인, 런타임 검사 및 설명서 생성을 제공합니다.

• 자동 테스트 도구: 코드 계약을 사용하여 사전 조건을 충족하지 않는 의미 없는 테스트 인수를 필터링하여 보다 의미 있는 단위 테스트를 생성할 수 있습니다.

• 정적 확인: 정적 검사기는 프로그램을 실행하지 않고 계약 위반이 있는지 여부를 결정할 수 있습니다. null 역참조와 배열 경계와 같은 암시적 계약, 및 명시적 계약을 확인합니다.

• 참조 설명서: 설명서 생성기는 계약 정보를 사용하여 기존 XML 설명서 파일을 보강합니다. 생성된 설명서 페이지에 계약 섹션이 있도록 샌드캐슬 과 함께 사용할 수 있는 스타일시트도 있습니다.

모든 .NET Framework 언어는 즉시 계약을 활용할 수 있습니다. 특수 파서 또는 컴파일러를 작성할 필요가 없습니다. Visual Studio 추가 기능을 사용하면 수행할 코드 계약 분석 수준을 지정할 수 있습니다. 분석기는 계약이 올바른 형식(형식 검사 및 이름 확인)임을 확인하고 CIL(공용 중간 언어) 형식으로 컴파일된 형태의 계약을 생성할 수 있습니다. Visual Studio에서 계약을 작성하면 도구에서 제공하는 표준 IntelliSense를 활용할 수 있습니다.

계약 클래스의 대부분의 메서드는 조건부로 컴파일됩니다. 즉, 컴파일러는 지시문을 사용하여 특수 기호 CONTRACTS_FULL 정의할 때만 이러한 메서드에 대한 호출을 #define 내보낸다. CONTRACTS_FULL 지시문을 사용하지 #ifdef 않고 코드에서 계약을 작성할 수 있습니다. 다른 빌드를 생성할 수 있고, 일부는 계약이 있고 일부는 없이 생성할 수 있습니다.

코드 계약 사용에 대한 도구 및 자세한 지침은 Visual Studio 마켓플레이 스 사이트의 코드 계약을 참조하세요.

전제 조건

메서드를 사용하여 Contract.Requires 사전 조건을 표현할 수 있습니다. 사전 조건은 메서드가 호출될 때 상태를 지정합니다. 일반적으로 유효한 매개 변수 값을 지정하는 데 사용됩니다. 사전 조건에 언급된 모든 멤버는 적어도 메서드 자체만큼 액세스 가능해야 합니다. 그렇지 않으면 메서드의 모든 호출자가 사전 조건을 이해하지 못할 수 있습니다. 조건에는 부작용이 없어야 합니다. 실패한 사전 조건의 런타임 동작은 런타임 분석기에서 결정됩니다.

예를 들어 다음 사전 조건은 해당 매개 변수 x 가 null이 아니어야 한다고 표현합니다.

Contract.Requires(x != null);

코드가 사전 조건 실패에 대해 특정 예외를 throw해야 하는 경우 다음과 같이 제네릭 오버로드를 Requires 사용할 수 있습니다.

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

레거시 요구 사항 문서

대부분의 코드는 코드 형식의 if-then-throw 일부 매개 변수 유효성 검사를 포함합니다. 계약 도구는 다음 경우 이러한 문을 전제 조건으로 인식합니다.

• 이 문장들은 메서드 내 다른 문장들보다 먼저 나타납니다.

• 이러한 문의 전체 집합 뒤에는 명시적 Contract 메서드 호출(예: Requires, Ensures, EnsuresOnThrow 또는 EndContractBlock 메서드 호출)이 있습니다.

문이 이 형식으로 표시되면 if-then-throw 도구는 이를 레거시 requires 문으로 인식합니다. 시퀀스를 따르는 if-then-throw 다른 계약이 없는 경우 메서드를 사용하여 코드를 종료합니다.Contract.EndContractBlock

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

이전 테스트의 조건은 부정된 전제 조건입니다. (실제 전제 조건은 x != null입니다.) 부정된 전제 조건은 매우 제한적입니다. 이전 예제와 같이 작성되어야 합니다. 즉, else 절을 포함하지 않아야 하며, then 절의 본문은 단일 throw 문으로 구성되어야 합니다. 테스트는 if 순도 규칙과 표시 유형 규칙( 사용 지침 참조)의 적용을 받지만 throw 식에는 순도 규칙만 적용됩니다. 그러나 던져진 예외의 타입은 계약이 발생하는 메서드만큼 가시적이어야 합니다.

사후 조건

사후 조건은 종료될 때 메서드의 상태에 대한 계약입니다. 사후 조건은 메서드를 종료하기 직전에 확인됩니다. 실패한 사후 조건의 런타임 동작은 런타임 분석기에서 결정됩니다.

사전 조건과 달리 사후 조건은 가시성이 낮은 멤버를 참조할 수 있습니다. 클라이언트는 프라이빗 상태를 사용하여 사후 조건으로 표현된 일부 정보를 이해하거나 사용하지 못할 수 있지만, 이는 메서드를 올바르게 사용하는 클라이언트의 기능에 영향을 주지 않습니다.

표준 사후 조건

메서드를 사용하여 Ensures 표준 사후 조건을 표현할 수 있습니다. 사후 조건은 메서드를 정상적으로 종료해야 true 하는 조건을 표현합니다.

Contract.Ensures(this.F > 0);

예외적인 사후 조건

예외적인 사후 조건은 메서드에 의해 특정 예외가 throw될 true 때 발생하는 사후 조건입니다. 다음 예제와 같이 메서드를 사용하여 Contract.EnsuresOnThrow 이러한 사후 조건을 지정할 수 있습니다.

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

인수는 형식 true의 하위 형식인 예외가 T를 던질 때마다 충족되어야 하는 조건입니다.

예외적인 사후 조건에 사용하기 어려운 몇 가지 예외 유형이 있습니다. 예를 들어 형식 Exception 을 T 사용하려면 스택 오버플로 또는 기타 제어할 수 없는 예외인 경우에도 throw되는 예외의 형식에 관계없이 조건을 보장하는 메서드가 필요합니다. 멤버가 호출될 때 발생할 수 있는 특정 예외가 있는 경우에만 예외적인 사후 조건을 사용해야 합니다. 예를 들어, InvalidTimeZoneException 메서드 호출 시 TimeZoneInfo가 발생할 때를 들 수 있습니다.

특별 사후 조건

다음 메서드는 사후 조건 내에서만 사용할 수 있습니다.

• 식을 Contract.Result<T>()사용하여 사후 조건의 메서드 반환 값을 참조할 수 있습니다. 여기서 T 메서드의 반환 형식으로 바뀝니다. 컴파일러가 형식을 유추할 수 없는 경우 명시적으로 제공해야 합니다. 예를 들어 C# 컴파일러는 인수를 사용하지 않는 메서드에 대해 형식을 유추할 수 없으므로 다음 사후 조건이 Contract.Ensures(0 <Contract.Result<int>()) 필요합니다. 반환 형식이 void 있는 메서드는 사후 조건에서 참조할 Contract.Result<T>() 수 없습니다.

• 사후 조건의 사전 상태 값은 메서드 또는 속성의 시작 부분에 있는 식의 값을 나타냅니다. 식을 Contract.OldValue<T>(e)사용합니다. 여기서 T 는 형식 e입니다. 컴파일러가 해당 형식을 유추할 수 있을 때마다 제네릭 형식 인수를 생략할 수 있습니다. 예를 들어 C# 컴파일러는 항상 인수를 사용하므로 형식을 유추합니다. 발생할 수 있는 e 항목과 이전 식이 나타날 수 있는 컨텍스트에 대한 몇 가지 제한 사항이 있습니다. 이전 식은 다른 이전 식을 포함할 수 없습니다. 가장 중요한 것은 이전 식이 메서드의 사전 조건 상태에 있는 값을 참조해야 한다는 것입니다. 즉, 메서드의 전제 조건이 true있는 한 계산할 수 있는 식이어야 합니다. 해당 규칙의 몇 가지 인스턴스는 다음과 같습니다.

  • 값은 메서드의 사전 조건 상태에 있어야 합니다. 개체의 필드를 참조하려면 사전 조건이 개체가 항상 null이 아닌지 확인해야 합니다.

  • 이전 식에서는 메서드의 반환 값을 참조할 수 없습니다.

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

  • 이전 식에서는 매개 변수를 참조할 out 수 없습니다.

  • 수량자의 범위가 메서드의 반환 값에 따라 달라지는 경우 이전 식은 수량자의 바인딩된 변수에 의존할 수 없습니다.

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

  • 기존 표현은 메서드 호출의 인덱서 또는 인수로 사용되지 않는 한 ForAll 또는 Exists 호출에서 익명 대리자의 매개 변수를 참조할 수 없습니다.

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

  • 익명 대리자가 ForAll 또는 Exists 메서드의 매개변수로 사용되지 않는 한, 이전 식의 값이 익명 대리자의 매개변수에 따라 달라지는 경우 익명 대리자의 본문에서 이전 식이 발생할 수 없습니다.

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

  • Out 매개 변수는 계약이 메서드 본문 앞에 나타나고 대부분의 컴파일러가 사후 조건의 매개 변수에 대한 참조를 out 허용하지 않기 때문에 문제가 발생합니다. 이 문제를 해결하기 위해 Contract 클래스는 ValueAtReturn 메서드를 제공하여 out 매개 변수를 기반으로 하는 사후 조건을 허용합니다.

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

    메서드와 OldValue 마찬가지로 컴파일러가 해당 형식을 유추할 수 있을 때마다 제네릭 형식 매개 변수를 생략할 수 있습니다. 계약 재작성기는 메서드 호출을 매개 변수 값 out 으로 바꿉니다. 메서드 ValueAtReturn는 사후 조건에만 나타날 수 있습니다. 메서드에 대한 인수는 out 매개 변수 또는 구조 out 매개 변수의 필드여야 합니다. 후자는 구조체 생성자의 사후 조건의 필드를 참조할 때도 유용합니다.

    비고

    현재 코드 계약 분석 도구는 매개 변수가 제대로 초기화되었는지 확인하지 않으며, 사후 조건에서의 언급을 무시합니다. 따라서 이전 예제에서 계약 후의 줄에서 정수 값을 할당하는 대신 x을 사용했다면, 컴파일러에서 적절한 오류 메시지를 발생시키지 않았을 것입니다. 그러나 CONTRACTS_FULL 전처리기 기호가 정의되지 않은 빌드에서(예: 릴리스 빌드) 컴파일러에서 오류가 발생합니다.

불변성

객체 불변식은 해당 객체가 클라이언트에 표시될 때마다 클래스의 각 인스턴스에 대해 참이어야 하는 조건입니다. 올바르다고 간주되는 개체의 조건을 표현합니다.

불변 메서드는 ContractInvariantMethodAttribute 특성으로 표시되어 식별됩니다. 고정 메서드는 다음 예제와 같이 각각 개별 고정을 지정하는 메서드에 대한 호출 Invariant 시퀀스를 제외하고 코드를 포함하지 않아야 합니다.

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

불변식은 조건부로 CONTRACTS_FULL 전처리기 기호에 의해 정의됩니다. 런타임 검사 중에는 각 공개 메서드의 끝에서 불변 조건이 검사됩니다. 불변식이 동일한 클래스의 public 메서드를 언급하는 경우, 해당 public 메서드의 끝에서 일반적으로 발생하는 불변식 검사는 비활성화됩니다. 대신, 검사는 해당 클래스에 대한 가장 바깥쪽 메서드 호출의 끝에만 발생합니다. 다른 클래스의 메서드 호출로 인해 클래스가 다시 입력되는 경우에도 발생합니다. 불변식은 객체 종료자 및 구현의 IDisposable.Dispose에 대해 검사되지 않습니다.

사용 지침

계약 순서 지정

다음 표에서는 메서드 계약을 작성할 때 사용해야 하는 요소의 순서를 보여 줍니다.

순도

계약 내에서 호출되는 모든 메서드는 순수해야 합니다. 즉, 기존 상태를 업데이트해서는 안됩니다. 순수 메서드는 순수 메서드에 입력한 후 만들어진 개체를 수정할 수 있습니다.

코드 계약 도구는 현재 다음 코드 요소가 순수하다고 가정합니다.

• 로 표시된 PureAttribute메서드입니다.

• 표시된 PureAttribute 형식(특성은 모든 형식의 메서드에 적용됨).

• 속성 가져오기 접근자입니다.

• 연산자(이름이 "op"로 시작되고 매개 변수가 하나 또는 두 개이고 void가 아닌 반환 형식이 있는 정적 메서드).

• 정규화된 이름이 "System.Diagnostics.Contracts.Contract", "System.String", "System.IO.Path" 또는 "System.Type"으로 시작하는 모든 메서드입니다.

• 대리자 형식 자체에 PureAttribute로 특성이 지정된 경우, 호출된 모든 대리자입니다. 대리자 형식 System.Predicate<T> 이며 System.Comparison<T> 순수로 간주됩니다.

가시성

계약에서 언급된 모든 멤버는 적어도 나타나는 메서드만큼 명시되어야 합니다. 예를 들어 public 메서드의 전제 조건에는 프라이빗 필드를 언급할 수 없습니다. 클라이언트는 메서드를 호출하기 전에 이러한 계약의 유효성을 검사할 수 없습니다. 그러나 필드가 표시된 ContractPublicPropertyNameAttribute경우 이러한 규칙에서 제외됩니다.

예시

다음 예제에서는 코드 계약의 사용을 보여 줍니다.

#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