Kódszerződések (.NET-keretrendszer)
Feljegyzés
Ez a cikk a .NET-keretrendszer vonatkozik. Ez nem vonatkozik a .NET újabb implementációira, beleértve a .NET 6-os és újabb verzióit.
A kódszerződések lehetővé teszik az előfeltételek, a postconditions és az objektum-invariánsok megadását .NET-keretrendszer kódban. Az előfeltételek olyan követelmények, amelyeket meg kell felelni egy metódus vagy tulajdonság megadásakor. A postconditions az elvárásokat írja le a metódus vagy a tulajdonságkód kilépésének időpontjában. Az objektum-invariánsok egy jó állapotú osztály várt állapotát írják le.
Feljegyzés
A kódszerződések nem támogatottak a .NET 5+-ban (beleértve a .NET Core-verziókat is). Fontolja meg a null értékű referenciatípusok használatát.
A kódszerződések tartalmazzák a kód megjelölésére szolgáló osztályokat, a fordítási idő elemzéséhez használt statikus elemzőt és egy futtatókörnyezet-elemzőt. A kódszerződések osztályai a System.Diagnostics.Contracts névtérben találhatók.
A kódszerződések előnyei a következők:
Továbbfejlesztett tesztelés: A kódszerződések statikus szerződés-ellenőrzést, futtatókörnyezet-ellenőrzést és dokumentáció-létrehozást biztosítanak.
Automatikus tesztelési eszközök: Kódszerződések használatával értelmesebb egységteszteket hozhat létre az előfeltételeknek nem megfelelő értelmetlen tesztargumentumok kiszűrésével.
Statikus ellenőrzés: A statikus ellenőrző el tudja dönteni, hogy vannak-e szerződésszegések a program futtatása nélkül. Implicit szerződéseket, például null hareferenseket, tömbkorlátokat és explicit szerződéseket keres.
Referenciadokumentáció: A dokumentációgenerátor kibővíti a meglévő XML-dokumentációs fájlokat szerződésadatokkal. Vannak olyan stíluslapok is, amelyek a Sandcastle használatával használhatók, így a létrehozott dokumentációs lapok szerződésszakaszokkal rendelkeznek.
Minden .NET-keretrendszer nyelv azonnal kihasználhatja a szerződések előnyeit; nem kell speciális elemzőt vagy fordítót írnia. A Visual Studio bővítmény lehetővé teszi a kódszerződések elemzésének szintjét. Az elemzők meggyőződhetnek arról, hogy a szerződések jól formázottak (típusellenőrzés és névfeloldás), és a szerződések lefordított formáját hozhatják létre közös köztes nyelven (CIL) formátumban. A Visual Studióban történő szerződések készítésével kihasználhatja az eszköz által biztosított standard IntelliSense előnyeit.
A szerződésosztály legtöbb metódusa feltételesen van lefordítva; vagyis a fordító csak akkor bocsát ki hívásokat ezekre a módszerekre, ha egy speciális szimbólumot határoz meg, CONTRACTS_FULL az #define irányelv használatával. CONTRACTS_FULL lehetővé teszi a szerződések írását a kódban irányelvek használata #ifdef nélkül; létrehozhat különböző buildeket, néhányat szerződésekkel, mások nélkül.
A kódszerződések használatára vonatkozó eszközöket és részletes utasításokat a Visual Studio piactéri webhelyén található Kódszerződések című témakörben találja.
Előfeltételek
A metódussal Contract.Requires előfeltételeket fejezhet ki. Az előfeltételek egy metódus meghívásának állapotát határozzák meg. Ezek általában érvényes paraméterértékek megadására szolgálnak. Az előfeltételekben említett tagoknak legalább olyan hozzáférhetőnek kell lenniük, mint maga a módszer; ellenkező esetben előfordulhat, hogy az előfeltételt nem minden hívó értelmezi. A feltételnek nem lehet mellékhatása. A sikertelen előfeltételek futásidejű viselkedését a futtatókörnyezet-elemző határozza meg.
Az alábbi előfeltétel például azt fejezi ki, hogy a paraméternek x nem null értékűnek kell lennie.
Contract.Requires(x != null);
Ha a kódnak kivételt kell kivennie egy előfeltétel meghibásodása esetén, az alábbiak szerint használhatja az általános túlterhelést Requires .
Contract.Requires<ArgumentNullException>(x != null, "x");
Az örökölt utasításhoz utasítások szükségesek
A legtöbb kód tartalmaz valamilyen paraméterérvényesítést if--thenthrow kód formájában. A szerződéses eszközök ezeket az utasításokat előfeltételekként ismerik fel a következő esetekben:
Az utasítások a metódus többi utasítása előtt jelennek meg.
Az ilyen utasítások teljes készletét explicit Contract metódushívás követi, például a Requires, Ensures, EnsuresOnThrowvagy EndContractBlock metódus hívása.
Amikor if--thenthrow az utasítások megjelennek ebben az formában, az eszközök régi requires utasításokként ismerik fel őket. Ha más szerződések nem követik a if--thenthrow sorrendet, fejezd be a kódot a Contract.EndContractBlock metódussal.
if (x == null) throw new ...
Contract.EndContractBlock(); // All previous "if" checks are preconditions
Vegye figyelembe, hogy az előző tesztben szereplő feltétel egy nem konfigurált előfeltétele. (A tényleges előfeltétele a . x != null) A nem konfigurált előfeltételek szigorúan korlátozottak: az előző példában látható módon kell megírni; azaz nem else tartalmazhat záradékokat, és a then záradék törzsének egyetlen throw utasításnak kell lennie. A if tesztre mind a tisztasági, mind a láthatósági szabályok vonatkoznak (lásd a használati útmutatót), de a throw kifejezésre csak tisztasági szabályok vonatkoznak. A kidobott kivétel típusának azonban ugyanolyan láthatónak kell lennie, mint a szerződés előfordulási módja.
Utókondíciók
A postconditions a metódus állapotára vonatkozó szerződés, amikor az leáll. A rendszer a metódus elhagyása előtt ellenőrzi az utókondíciót. A sikertelen postconditions futásidejű viselkedését a futtatókörnyezet-elemző határozza meg.
Az előfeltételektől eltérően a posztkondíciók kevésbé ismert tagokra hivatkozhatnak. Előfordulhat, hogy az ügyfél nem tudja megérteni vagy felhasználni a privát állapotot használó utókondíció által kifejezett információk egy részét, de ez nem befolyásolja az ügyfél azon képességét, hogy helyesen használja a módszert.
Standard Postconditions
A módszer használatával Ensures szabványos utókondicionálásokat fejezhet ki. A posztkondíciók olyan feltételt fejeznek ki, amelyet a módszer normál leállásakor kell megadni true .
Contract.Ensures(this.F > 0);
Kivételes utókondíciók
A kivételes posztkondíciók olyan posztkondíciók, amelyeknek akkor kell lenniük true , ha egy adott kivételt egy metódus alkalmaz. Ezeket az utókondicionálásokat a Contract.EnsuresOnThrow metódussal adhatja meg, ahogy az alábbi példa is mutatja.
Contract.EnsuresOnThrow<T>(this.F > 0);
Az argumentum az a feltétel, amely akkor lehet true , ha a rendszer kivételt ad, amely egy altípusa T .
Vannak olyan kivételtípusok, amelyeket nehéz használni egy kivételes utókondícióban. Ha például a típust ExceptionT használja, a metódusnak garantálnia kell a feltételt a kidobott kivétel típusától függetlenül, még akkor is, ha az egy verem túlcsordulása vagy más lehetetlen kivétel. Kivételes utókondicionálásokat csak olyan kivételek esetén érdemes használni, amelyek egy tag meghívásakor, például egy metódushíváshoz TimeZoneInfo való dobáskor InvalidTimeZoneException fordulhatnak elő.
Speciális utókondíciók
A következő módszerek csak utókondíciókon belül használhatók:
Az utókondíciókban a metódus visszatérési értékeire a kifejezéssel
Contract.Result<T>()hivatkozhat, aholTa metódus visszatérési típusa váltja fel. Ha a fordító nem tudja kikövetkeztetni a típust, explicit módon kell megadnia. A C#-fordító például nem tud olyan metódustípusokat kikövetkeztetni, amelyek nem vesznek fel argumentumokat, ezért a következő utókondicionálást igényli:Contract.Ensures(0 <Contract.Result<int>())A visszatérésivoidtípusú metódusok nem hivatkozhatnakContract.Result<T>()az utókondicionálásokban.A postcondition prestate értéke egy metódus vagy tulajdonság elején lévő kifejezés értékére utal. A kifejezést
Contract.OldValue<T>(e)használja , aholTa típuse. Kihagyhatja az általános típusargumentumot, ha a fordító képes a típusára következtetni. (A C#-fordító például mindig a típusra következtet, mert argumentumot vesz igénybe.) Számos korlátozás van arra, hogy mi történhet,eés hogy milyen környezetekben jelenhet meg egy régi kifejezés. A régi kifejezések nem tartalmazhatnak másik régi kifejezést. A legfontosabb, hogy egy régi kifejezésnek olyan értékre kell hivatkoznia, amely a metódus előfeltételeinek állapotában létezett. Más szóval olyan kifejezésnek kell lennie, amely kiértékelhető mindaddig, amíg a metódus előfeltétele .trueAz alábbiakban a szabály több példányát is bemutatjuk.Az értéknek a metódus előfeltételeinek állapotában kell lennie. Ahhoz, hogy egy objektumon lévő mezőre hivatkozhasson, az előfeltételeknek garantálniuk kell, hogy az objektum mindig nem null értékű.
Egy régi kifejezésben nem hivatkozhat a metódus visszatérési értékére:
Contract.OldValue(Contract.Result<int>() + x) // ERRORRégi kifejezésben nem hivatkozhat
outparaméterekre.Egy régi kifejezés nem függhet a kvantáló kötött változójától, ha a kvantáló tartománya a metódus visszatérési értékétől függ:
Contract.ForAll(0, Contract.Result<int>(), i => Contract.OldValue(xs[i]) > 3); // ERROREgy régi kifejezés csak akkor hivatkozhat a névtelen meghatalmazott paraméterére egy ForAll hívásban vagy Exists hívásban, ha azt indexelőként vagy argumentumként használják metódushíváshoz:
Contract.ForAll(0, xs.Length, i => Contract.OldValue(xs[i]) > 3); // OK Contract.ForAll(0, xs.Length, i => Contract.OldValue(i) > 3); // ERRORA névtelen meghatalmazott törzsében nem fordulhat elő régi kifejezés, ha a régi kifejezés értéke a névtelen meghatalmazott egyik paraméterétől függ, kivéve, ha a névtelen meghatalmazott argumentuma a ForAll metódusnak:Exists
Method(... (T t) => Contract.OldValue(... t ...) ...); // ERROROuta paraméterek problémát okoznak, mert a szerződések a metódus törzse előtt jelennek meg, és a legtöbb fordító nem engedélyezi a paraméterekreoutvaló hivatkozást az utókondíciókban. A probléma megoldásához az osztály biztosítja a ContractValueAtReturn metódust, amely lehetővé teszi a paraméteren alapuló utólagos kondíciótout.public void OutParam(out int x) { Contract.Ensures(Contract.ValueAtReturn(out x) == 3); x = 3; }A metódushoz OldValue hasonlóan kihagyhatja az általános típusparamétert, amikor a fordító képes a típusára következtetni. A szerződés újraírója a metódushívást a paraméter értékére cseréli
out. A ValueAtReturn metódus csak utókondíciókban jelenhet meg. A metódus argumentumának egyoutparaméternek vagy egy struktúraparaméteroutmezőjének kell lennie. Ez utóbbi akkor is hasznos, ha egy struktúrakonstruktor utókonfigurálásának mezőire hivatkozik.Feljegyzés
A kódszerződés-elemző eszközök jelenleg nem ellenőrzik, hogy a paraméterek inicializálása megfelelően van-e, és figyelmen kívül hagyják-e
outa postconditionban való említést. Ezért az előző példában, ha a szerződés utáni sor az egész szám hozzárendelésexhelyett az értéket használta volna, akkor a fordító nem a megfelelő hibát adná ki. Olyan buildek esetében azonban, amelyekben nincs definiálva az CONTRACTS_FULL előfeldolgozó szimbólum (például kiadási build), a fordító hibát fog okozni.
Invariánsok
Az objektum-invariánsok olyan feltételek, amelyeknek igaznak kell lenniük egy osztály minden példányára, amikor az objektum látható az ügyfél számára. Kifejezik azokat a feltételeket, amelyek alapján az objektum helyesnek tekinthető.
Az invariáns metódusokat az ContractInvariantMethodAttribute attribútummal jelöltük meg. Az invariáns metódusoknak nem tartalmazhatnak kódot, kivéve a Invariant metódushoz intézett hívások sorozatát, amelyek mindegyike egy-egy invariánst határoz meg az alábbi példában látható módon.
[ContractInvariantMethod]
protected void ObjectInvariant ()
{
Contract.Invariant(this.y >= 0);
Contract.Invariant(this.x > this.y);
...
}
Az invariánsokat feltételesen az CONTRACTS_FULL előfeldolgozó szimbólum határozza meg. A futásidejű ellenőrzés során a rendszer minden nyilvános módszer végén ellenőrzi a változókat. Ha egy invariáns egy nyilvános metódust említ ugyanabban az osztályban, a nyilvános metódus végén általában előforduló invariáns ellenőrzés le van tiltva. Ehelyett az ellenőrzés csak az adott osztályra irányuló legkülső metódushívás végén történik. Ez akkor is előfordul, ha az osztály újra be van írva egy másik osztály metódusának hívása miatt. Az invariánsok nem ellenőrzik az objektum-véglegesítőt és a megvalósítást IDisposable.Dispose .
Használati irányelvek
Szerződés megrendelése
Az alábbi táblázat a metódusszerződések írásakor használandó elemek sorrendjét mutatja be.
If-then-throw statements |
Visszamenőlegesen kompatibilis nyilvános előfeltételek |
|---|---|
| Requires | Minden nyilvános előfeltétel. |
| Ensures | Minden nyilvános (normál) utókondíció. |
| EnsuresOnThrow | Minden nyilvános kivételes utókondíció. |
| Ensures | Minden privát/belső (normál) utókondíció. |
| EnsuresOnThrow | Minden privát/belső kivételes utókondíció. |
| EndContractBlock | Ha más szerződés nélküli stíluselőfeltételeket használif--thenthrow, hívjon EndContractBlock fel egy hívást, amely jelzi, hogy az összes korábbi ellenőrzés előfeltételei-e. |
Tisztaság
A szerződésben lehívott összes metódusnak tisztanak kell lennie; vagyis nem frissíthetnek semmilyen már létező állapotot. A tiszta metódusok módosíthatják a tiszta metódusba való belépés után létrehozott objektumokat.
A kódszerződés eszközei jelenleg feltételezik, hogy a következő kódelemek tisztaak:
A következővel PureAttribute megjelölt típusok (az attribútum a típus összes metódusára vonatkozik).
A tulajdonsághoz kellékek lekérése.
Operátorok (statikus metódusok, amelyeknek a neve "op" néven kezdődik, és amelyek egy vagy két paraméterrel és nem érvénytelen visszatérési típussal rendelkeznek).
Bármely metódus, amelynek teljes neve "System.Diagnostics.Contracts.Contract", "System.String", "System.IO.Path" vagy "System.Type" néven kezdődik.
Bármely meghívott delegált, feltéve, hogy a delegált típusa a PureAttribute. A delegált típusok System.Predicate<T> , és System.Comparison<T> tisztanak minősülnek.
Látótávolság
A szerződésben említett összes tagnak legalább olyan láthatónak kell lennie, mint az a módszer, amelyben megjelennek. Nyilvános metódus előfeltételei között például nem szerepelhet magánmező; az ügyfelek nem tudják érvényesíteni az ilyen szerződést, mielőtt meghívják a metódust. Ha azonban a mező a következővel ContractPublicPropertyNameAttributevan megjelölve, akkor mentesül ezek alól a szabályok alól.
Példa
Az alábbi példa a kódszerződések használatát mutatja be.
#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
