코드 계약
코드 계약은 코드에서 사전 조건, 사후 조건 및 개체 고정을 지정하는 방법을 제공합니다. 사전 조건은 메서드나 속성을 입력할 때 충족되어야 하는 요구 사항입니다. 사후 조건은 메서드 또는 속성 코드가 존재하는 시점에 대하여 예상되는 상태입니다. 개체 고정은 올바른 상태의 클래스에 대하여 예상되는 상태를 나타냅니다.
코드 계약에는 코드를 표시하기 위한 클래스, 컴파일 타임 분석을 위한 정적 분석기, 런타임 분석기 등이 포함되어 있습니다. 코드 계약의 클래스는 System.Diagnostics.Contracts 네임스페이스에서 찾을 수 있습니다.
코드 계약의 이점은 다음과 같습니다.
테스트 성능 향상: 코드 계약은 정적 계약 확인, 런타임 검사, 문서 생성 기능을 제공합니다.
자동 테스트 도구: 코드 계약을 사용하여 사전 조건을 충족하지 않는 의미 없는 테스트 인수를 필터링하여 보다 의미 있는 단위 테스트를 생성할 수 있습니다.
정적 확인: 정적 검사기는 프로그램을 실행하지 않고도 계약 위반이 있는지를 파악할 수 있습니다. null 역참조 및 배열 범위 같은 암시적 계약과 명시적 계약을 검사합니다.
참조 설명서: 설명서 생성기는 계약 정보를 사용하여 기존 XML 설명서 파일을 확장합니다. 생성된 설명서 페이지에 계약 섹션이 포함되도록 Sandcastle과 함께 사용할 수 있는 스타일시트도 있습니다.
모든 .NET Framework 언어는 계약을 바로 이용할 수 있으므로 특별한 파서 또는 컴파일러를 작성할 필요가 없습니다. Visual Studio 추가 기능을 사용하면 수행할 코드 계약 분석의 수준을 지정할 수 있습니다. 분석기는 계약의 형식이 올바른지 확인하고(형식 검사 및 이름 확인) 계약의 컴파일된 양식을 MSIL(Microsoft Intermediate Language) 형식으로 만들 수 있습니다. Visual Studio로 계약을 만들면 Visual Studio에서 제공하는 표준 IntelliSense를 이용할 수 있습니다.
계약 클래스에 있는 대부분의 메서드는 조건부로 컴파일됩니다. 즉, 컴파일러는 사용자가 #define 지시문을 사용하여 특수 기호, CONTRACTS FULL을 정의한 경우에만 해당 메서드에 대한 호출을 내보냅니다. CONTRACTS FULL을 정의하면 #ifdef 지시문을 사용하지 않고도 코드에 계약을 쓸 수 있습니다. 계약이 있거나 없는 여러 가지 빌드를 만들 수 있습니다.
코드 계약을 사용하기 위한 도구 및 자세한 지침은 MSDN DevLabs 웹 사이트에서 코드 계약을 참조하십시오.
사전 조건
Contract.Requires 메서드를 사용하여 사전 조건을 나타낼 수 있습니다. 사전 조건은 메서드가 호출될 때의 상태를 지정합니다. 또한 일반적으로 유효한 매개 변수 값을 지정하는 데 사용됩니다. 사전 조건에 명시된 모든 멤버의 액세스 가능성은 최소한 메서드와 같은 수준이어야 합니다. 그렇지 않으면 메서드의 일부 호출자가 사전 조건을 인식하지 못할 수 있습니다. 조건에는 부수적 효과가 없어야 합니다. 실패한 사전 조건의 런타임 동작은 런타임 분석기에 의해 결정됩니다.
예를 들어 다음 사전 조건은 x 매개 변수가 null이 아니어야 함을 나타냅니다.
Contract.Requires( x != null );
코드가 사전 조건의 실패에 대해 특정 예외를 throw해야 하는 경우 다음과 같이 Requires의 제네릭 오버로드를 사용할 수 있습니다.
Contract.Requires<ArgumentNullException>( x != null, "x" );
레거시 Requires 문
대부분의 코드에는 if-then-throw 코드 형식의 몇 가지 매개 변수 유효성 검사가 포함되어 있습니다. 계약 도구는 다음과 같은 경우에 이러한 문을 사전 조건으로 인식합니다.
문이 메서드에서 다른 문 앞에 나타납니다.
이러한 문의 전체 집합 뒤에는 Requires, Ensures, EnsuresOnThrow, EndContractBlock 메서드 등 명시적인 Contract 메서드 호출이 나옵니다.
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 식은 순수성 규칙만 따릅니다. 하지만 throw된 예외의 형식은 계약이 포함된 메서드와 같은 수준으로 표시되어야 합니다.
사후 조건
사후 조건은 메서드가 종료될 때의 상태에 대한 계약입니다. 사후 조건은 메서드가 종료되기 전에 검사됩니다. 실패한 사후 조건의 런타임 동작은 런타임 분석기에 의해 결정됩니다.
사전 조건과 달리 사후 조건은 표시 유형이 제한적인 멤버를 참조할 수 있습니다. 클라이언트는 전용 상태를 사용하여 사후 조건에서 표시하는 정보 중 일부를 인식하지 못하거나 사용하지 못할 수도 있지만, 이는 클라이언트가 메서드를 올바르게 사용하는 데는 영향을 주지 않습니다.
표준 사후 조건
Ensures 메서드를 사용하여 표준 사후 조건을 나타낼 수 있습니다. 사후 조건은 메서드가 종료될 때 true여야 하는 조건을 나타냅니다.
Contract.Ensures( this .F > 0 );
예외 사후 조건
예외 사후 조건은 메서드가 특정 예외를 throw할 때 true여야 하는 사후 조건입니다. 다음 예제와 같이 Contract.EnsuresOnThrow 메서드를 사용하여 이러한 사후 조건을 지정할 수 있습니다.
Contract.EnsuresOnThrow<T>( this.F > 0 );
인수는 하위 형식이 T인 예외가 throw될 때마다 true여야 하는 조건입니다.
예외 사후 조건에서 사용하기 어려운 몇 가지 예외 형식이 있습니다. 예를 들어 Exception 형식을 T에 대해 사용하려면 throw되는 예외의 형식에 관계없이 메서드가 조건을 보장해야 합니다. 스택 오버플로이거나 제어 불가능한 기타 예외인 경우에도 마찬가지입니다. InvalidTimeZoneException이 TimeZoneInfo 메서드 호출에 대해 throw되는 경우와 같이 멤버가 호출될 때 throw될 수 있는 특정 예외에 대해서만 예외 사후 조건을 사용해야 합니다.
특수 사후 조건
다음 메서드는 사후 조건 내에서만 사용할 수 있습니다.
Contract. Result<T>() 식을 사용하여 사후 조건에서 메서드 반환 값을 참조할 수 있습니다. 여기서 T는 메서드의 반환 형식으로 대체됩니다. 컴파일러가 형식을 유추할 수 없을 때는 명시적으로 제공되어야 합니다. 예를 들어 C# 컴파일러는 인수를 사용하지 않는 메서드의 형식을 유추할 수 없습니다. 따라서 다음 사후 조건이 필요합니다. 반환 형식이 void인 Contract.Ensures(0 < Contract.Result<int>()) 메서드는 사후 조건에서 Contract. Result<T>()를 참조할 수 없습니다.
사후 조건에서 사전 상태 값은 메서드 또는 속성의 시작 부분에 있는 식의 값을 나타냅니다. Contract.OldValue<T>(e) 식을 사용합니다. 여기서 T는 e의 형식입니다. 컴파일러가 형식을 유추할 수 있을 때는 항상 제네릭 형식 인수를 생략할 수 있습니다. 예를 들어 C# 컴파일러는 인수를 사용하기 때문에 항상 형식을 유추합니다. e에 포함될 수 있는 내용과 old 식이 나타날 수 있는 컨텍스트에는 몇 가지 제한이 있습니다. old 식은 다른 old 식을 포함할 수 없습니다. 보다 중요한 것은 old 식이 메서드의 사전 조건 상태에 있었던 값을 참조해야 한다는 것입니다. 다시 말해 메서드의 사전 조건이 true인 경우에만 평가될 수 있는 식이어야 합니다. 다음은 이러한 규칙의 몇 가지 예입니다.
값은 메서드의 사전 조건 상태 안에 있어야 합니다. 개체에서 필드를 참조하기 위해서는 해당 개체가 항상 null이 아니라는 것을 사전 조건이 보장해야 합니다.
old 식에서는 메서드의 반환 값을 참조할 수 없습니다.
Contract.OldValue(Contract.Result<int>() + x) // ERRORold 식에서는 out 매개 변수를 참조할 수 없습니다.
수량자의 범위가 메서드의 반환 값에 따라 달라지는 경우 old 식은 해당 수량자의 바인딩된 변수에 종속될 수 없습니다.
Contract. ForAll (0,Contract. Result<int>(), i => Contract.OldValue(xs[i]) > 3 ); // ERROR메서드 호출에 대해 인덱서나 인수로 사용되는 경우를 제외하고 old 식은 ForAll 또는 Exists 호출에서 익명 대리자의 매개 변수를 참조할 수 없습니다.
Contract. ForAll (0, xs .Length, i => Contract.OldValue(xs[i]) > 3); // OK Contract. ForAll (0, xs .Length, i => Contract.OldValue(i) > 3 ); // ERRORold 식의 값이 익명 대리자의 매개 변수에 따라 달라지는 경우 old 식은 익명 대리자의 본문에 포함될 수 없습니다. 단, 해당 익명 대리자가 ForAll 또는 Exists 메서드에 대한 인수인 경우는 예외입니다.
Method( ... (T t) => Contract.OldValue(... t ...) ... ); // ERROR계약이 메서드 본문 앞에 나타나고 대부분의 컴파일러는 사후 조건에서 out 매개 변수에 대한 참조를 허용하지 않기 때문에 Out 매개 변수가 문제를 일으킵니다. 이 문제를 해결하기 위해 Contract 클래스는 out 매개 변수를 기반으로 사후 조건을 허용하는 ValueAtReturn<T> 메서드를 제공합니다.
public void OutParam(out int x) f Contract.Ensures(Contract.ValueAtReturn(out x) == 3); x = 3;OldValue<T> 메서드에서와 마찬가지로 컴파일러가 형식을 유추할 수 있을 때는 항상 제네릭 형식 매개 변수를 생략할 수 있습니다. 계약 재작성기는 메서드 호출을 out 매개 변수의 값으로 대체합니다. ValueAtReturn<T> 메서드는 사후 조건에서만 나타날 수 있습니다. 메서드에 대한 인수는 out 매개 변수이거나 구조 out 매개 변수의 필드여야 합니다. 후자는 구조 생성자의 사후 조건에서 필드를 참조할 때도 유용합니다.
.gif "참고")
참고현재 코드 계약 분석기 도구는 out 매개 변수가 올바르게 초기화되는지 여부를 검사하지 않으며 사후 조건에서 해당 내용을 무시합니다.따라서 이전 예제에서 계약 뒤의 줄이 정수를 할당하는 대신 x 값을 사용했다면 컴파일러가 올바른 오류를 생성하지 못했을 것입니다.하지만 CONTRACTS FULL 전처리기 기호가 정의되어 있지 않은 빌드(예:릴리스 빌드)에서는 컴파일러에서 오류를 생성할 것입니다.
고정 조건
개체 고정은 개체가 클라이언트에 표시될 때 클래스의 각 인스턴스에 대해 true여야 하는 조건입니다. 개체가 올바르다고 간주되는 조건을 나타냅니다.
고정 메서드는 ContractInvariantMethodAttribute 특성으로 표시되어 구분됩니다. 고정 메서드는 다음 예제와 같이 각각 개별 개체 고정을 지정하는 Invariant 메서드 호출의 시퀀스를 제외하고는 코드를 포함하지 않아야 합니다.
[ContractInvariantMethod]
protected void ObjectInvariant ()
{
Contract.Invariant ( this.y >= 0 );
Contract.Invariant ( this.x > this.y );
...
}
개체 고정은 CONTRACTS FULL 전처리기 기호에 의해 조건부로 정의됩니다. 런타임 검사 동안 개체 고정은 각 public 메서드의 끝에서 검사됩니다. 개체 고정에서 같은 클래스에 있는 public 메서드가 명시된 경우에는 해당 public 메서드의 끝에서 일반적으로 수행되는 개체 고정 검사를 사용할 수 없는 것입니다. 대신 해당 클래스의 가장 바깥쪽에 있는 메서드 호출의 끝에서만 검사가 이루어집니다. 다른 클래스에 있는 메서드에 대한 호출로 인해 클래스가 다시 입력된 경우에도 이러한 상황이 발생합니다. 개체 종료자 또는 Dispose 메서드를 구현하는 메서드에 대해서는 개체 고정을 검사하지 않습니다.
사용 지침
계약 순서 지정
다음 표에서는 메서드 계약을 쓸 때 사용해야 하는 요소의 순서를 보여 줍니다.
If-then-throw statements |
이전 버전과 호환되는 공용 사전 조건 |
모든 공용 사전 조건 |
|
모든 공용(일반) 사전 조건 |
|
모든 공용 예외 사전 조건 |
|
모든 전용/내부(일반) 사전 조건 |
|
모든 전용/내부 예외 사전 조건 |
|
if-then-throw 스타일 사전 조건을 다른 계약 없이 사용하는 경우에는 EndContractBlock 호출을 넣어서 이전의 모든 if 검사가 사전 조건임을 나타내십시오. |
순수성
계약 내에서 호출되는 모든 메서드는 순수해야 합니다. 즉, 기존 상태를 업데이트하지 않아야 합니다. 순수 메서드는 순수 메서드로 진입한 이후에 만들어진 개체를 수정할 수는 있습니다.
코드 계약 도구는 현재 다음 코드 요소가 순수하다고 가정합니다.
PureAttribute로 표시된 메서드
PureAttribute로 표시된 형식(특성이 모든 형식의 메서드에 적용됨)
Property get 접근자
연산자(이름이 "op"로 시작되고 하나 또는 두 개의 매개 변수와 void가 아닌 반환 형식을 가지고 있는 정적 메서드)
정규화된 이름이 "System.Diagnostics.Contracts.Contract", "System.String", "System.IO.Path" 또는 "System.Type"으로 시작되는 메서드
대리자 형식 자체가 PureAttribute로 지정된 경우의 호출된 대리자 대리자 형식 System.Predicate<T> 및 System.Comparison<T>은 순수한 것으로 간주됩니다.
표시 유형
계약에 명시된 모든 멤버는 최소한 해당 멤버가 나타나는 메서드와 같은 수준으로 표시되어야 합니다. 예를 들어 public 메서드의 사전 조건에서는 전용 필드가 명시될 수 없습니다. 클라이언트는 메서드를 호출하기 전에 이러한 계약의 유효성을 검사할 수 없습니다. 하지만 필드가 ContractPublicPropertyNameAttribute로 표시되어 있으면 이러한 규칙에서 제외됩니다.
예제
다음 예제에서는 코드 계약을 사용하는 방법을 보여 줍니다.
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);
}
}