Szerződések (Contracts)
A programozási nyelv nyelvhelyesség ellenőrzést támogató metódusai a Contract osztályban találhatóak meg, ami System.Diagnostics.Contracts névtérben helyezkedik el. Ennek az osztálynak a segítségével lehetőség van előfeltételek, utófeltételek és invariánsok megadására. Részletes ismertetés előtt nézzünk egy egyszerű példát, ami segít megismerni a fontosabb fogalmakat. A lejjebb található kód a racionális számot megvalósító osztály egy része. A legfontosabb feltétel, aminek teljesülnie kell ennél a típusnál, hogy a nevező nem lehet nulla. Ennek ellenőrzésére szolgál a konstruktorban elhelyezett előfeltétel (Contract.Requires), az ObjectInvariant metódus, mint invariáns (amit a ContractInvariantMethod attribútummal jelölünk), valamint a Nevezo property-ben szereplő utófeltétel (Contract.Ensures)
using System;
using System.Diagnostics.Contracts;
namespace ContractExample1
{
class Racionalis
{
int szamlalo;
int nevezo;
public Racionalis(int szamlalo, int nevezo)
{
Contract.Requires(nevezo != 0);
this.szamlalo = szamlalo;
this.nevezo = nevezo;
}
public int Nevezo
{
get
{
Contract.Ensures(Contract.Result() != 0);
return this.nevezo;
}
}
[ContractInvariantMethod]
protected void ObjectInvariant()
{
Contract.Invariant(this.nevezo != 0);
}
}
}
Előfeltételek (Preconditions)
Az előfeltételek kifejezésére szolgál a Contract.Requires(…) metódus. Ezt általában paraméterek ellenőrzésére szokás használni. Az előfeltételben szereplő összes tagnak elérhetőnek kell lennie az adott helyen, különben az előfeltételt nem tudja értelmezni a hívó metódus. A megadott feltételeknek nem lehet mellékhatásuk. A következő előfeltétel az fejezi ki, hogy az x paraméter nem lehet null:
Contract.Requires( x ! = null );
Lehetőség van arra is, hogy megadjuk, hogy ha az adott feltétel nem teljesül akkor milyen kivétel váltodjok ki:
Contract.Requires( x != null );
Örökölt követelmények (Legacy Requires)
A legtöbb kódban a paraméterek ellenőrzésére if-then-throw szerkezetet használnak. Szerencsére ezeket egyszerű módon át lehet alakítani előfeltételekké, abban az esetben, ha ezek az utasítások a metódus elején találhatóak és egy explicit contract metódushívás (mint például: Requires, Ensures, EnsuresOnThrow vagy EndContractBlock) követi őket. Az ilyen if-then-throw szerkezeteket nevezzük örökölt követelményeknek.
if ( x == null ) throw new ...
Contract.EndContractBlock(); // All previous ' if ' checks are preconditions
Utófeltételek (Postconditions)
Az utófeltétel ellenőrzése az adott metódus végrehajtása után történik meg.
Közönséges utófeltételek (Normal Postconditions)
Egy közönséges utófeltételt a Contract.Ensures() kifejezéssel írunk le. Ezzel olyan feltételt fejezzük ki, aminek a metódus végrehajtása után kell teljesülnie.
Contract.Ensures( this .F > 0 );
Kivételes utófeltételek (Exceptional Postconditions)
Ha a metódus végrehajtása során kivétel váltódik ki, akkor is lehetőség van az utófeltétel ellenőrzésére. Ekkor a kivétel típusától függően is lehet megadni feltételt.
Contract.EnsuresOnThrow( this.F > 0 );
Ebben az esetben, ha a T típusú kivétel váltódik ki, akkor a fordító leellenőrzi, hogy teljesül-e a megadott feltétel.
Speciális metódusok az utófeltételben
Létezik néhány metódus, amit csak utófeltételek belsejében lehet használni.
Contract.Result
Ez a metódus a T típusú visszatérési értéket adja meg. T-t csak abban az esetben kell
megadni, ha a fordító nem tudja kikövetkeztetni a típust. A void típusú függvényeknél ez a
kifejezés nem használható.
Contract.Ensures(0 < Contract.Result());
Contract.OldValue
Ez a T típusú e kifejezés metódus hívása előtt értékét adja vissza. A T-t itt is csak akkor
kell megadni, ha azt a fordító nem tudja kikövetkeztetni a típust. Az adott kifejezés régi
értékét csak az utófeltételben lehet használni és van néhány fontos megkötés: az e kifejezés
nem tartalmazhat másik régi értéket lekérdező függvényt és csak olyan kifejezésre hivatkozhat,
aminek létezet értéke a metódus meghívása előtt. Néhány példa az előbbi szabályokra:
1. A metódus visszatérési értékének a régi értékére nem lehet hivatkozni.
Contract.OldValue(Contract.Result() + x) // ERROR
2. Legyen az előfeltétel (xs ! = null || E). Ebben az esetben az alábbi kifejezés hibás lesz,ha xs–nek nem volt éréke az adott metódus hívása előtt, és az E miatt az előfeltétel teljesül.
Contract.OldValue(xs.Length) // POSSIBLE ERROR
3. Out paraméternek nem lehet a régi értékére hivatkozni.
4. A régi érték nem függhet a visszatérési értéktől.
Contract.ForAll(0,Contract.Result(),i => Contract.OldValue(xs[i]) > 3 ); // ERROR
5. A régi érték kifejezés nem tartalmazhat egy névtelen delegálthoz tartozó paramétert a Contract.ForAll vagy Contract.Exists utasításokban, hacsak nem metódus paraméterként vagy index változóként szerepel.
Contract.ForAll(0, xs .Length, i => Contract.OldValue(xs[i]) > 3); // OK
Contract.ForAll(0, xs .Length, i => Contract.OldValue(i) > 3 ); // ERROR
6. A régi érték kifejezése nem szerepelhet névtelen delegált törzsében, ha a delegált valamelyik paraméterétől függ, hacsak nem a Contract.Exists vagy a Contract.ForAll kifejezés egy argumentuma.
Foo( ... (T t) => Contract.OldValue(... t ...) ... ); // ERROR
Contract.ValueAtReturn
Ennek segítségével lehetőség van az out paraméter értékének ellenőrzésére az utófeltételben.
Csak kimenő paramétereknél használható. A T típust csak akkor kell megadni, ha azt a
fordító nem tudja kikövetkeztetni.
public void OutParam(out int x)
{
Contract.Ensures(Contract.ValueAtReturn(out x) == 3);
x = 3;
}
Invariánsok (Invariants)
Az invariánsok olyan feltételek halmaza, amelyeknek mindig teljesülnie kell az adott objektumra. Az összes invariánsnak void típusú függvények kell lennie, és ha az adott osztályból lehet származtatni, akkor a láthatóságnak protected-et kell megadni. A [ContractInvariantMethod] attribútummal jelöljük, hogy az adott metódus egy invariáns, és ekkor ez nem tartalmazhat invariáns függvényt meghívó utasítást.
[ContractInvariantMethod]
protected void ObjectInvariant()
{
Contract.Invariant( this.y >= 0 );
Contract.Invariant( this.x > this.y );
...
}
Az invariáns ellenőrzése az össze publikus metódus végrehajtása után megtörténik. Ha az invariánson belül hivatkozunk az osztály egy másik publikus metódusára, akkor csak a legkülső függvénynél történik ellenőrzés.
Assert
Különböző állításokat lehet megfogalmazni a Contract.Assert kifejezés segítségével. Ezzel a program egy bizonyos pontján tudjuk ellenőrizni, hogy a megadott állítás teljesül-e.
Contract.Assert( this.privateField > 0 );
Contract.Assert( this.x == 3, "Why isn't the value of x 3?" );
Assume
Egy feltevést lehet leírni a Contract.Assume kifejezéssel. Ennek a működése megegyezik az Assert-tel futási időben, azonban ez leállítja a program fordítását, ha az adott feltétel nem teljesül fordítási időben.
Contract.Assume( this.privateField > 0 );
Contract.Assume( this.x == 3, "Static checker assumed this");
EndContractBlock
Ha a metódus előfeltételeinek ellenőrzése if-then-throw formában vannak leírva, akkor a Contract.EndContractBlock utasítás segítségével jelezzük, hogy ezeket az utasításokat előfeltételként kell kezelni és itt van az ellenőrző blokk vége.
if ( x == null ) throw new ArgumentNullException("x");
if ( y < 0 ) throw new ArgumentOutOfRangeException(...);
Contract.EndContractBlock( );
ForAll
Ez egy léptető ciklus, amit egy contract-on belül lehet használni. Két változata van, az egyiknél két paramétert a másiknál pedig három paramétert kell megadni.
public int Foo(IEnumerable xs){
Contract.Requires(Contract.ForAll( xs, (T x) => x != null) );
A két paraméteres változatnál az első paraméter egy kollekció a második egy predikátum. A predikátum egy olyan függvény, aminek a visszatérési értéke logikai típusú. Ha a predikátum igaz a kollekció minden elemére, akkor igaz értékkel tér vissza ez a függvény, azonban ha egy elemre nem teljesül a megadott feltétel, akkor a ForAll megáll és hamis értékkel tér vissza.
public int[] Bar(){
Contract.Ensures( Contract.ForAll(0, Contract.Result().Length, index => Contract.Result()[index] > 0));
A három paraméteres változatnál az első paraméter az alsó index, a második a felső index a harmadik pedig a predikátum. Ekkor a két index között bejárja az adott kollekció elemei a ForAll metódus. A predikátum argumentumában szerepelnie kell egy integer típusú változónak, ami a futó indexet jelenti.
Exists
Contract. Exists kifejezésnek ugyanolyan paraméterei vannak, mint a ForAll metódusnak. Működése is hasonló azonban ez akkor tér vissza igaz értékkel, ha a kollekció legalább egy elemére teljesül az adott predikátum és hamis értékkel tér vissza, ha egyetlen egy elemre sem teljesül.
Interfész contract-ok
Interfészekhez is lehet megadni contract-ot, azonban mivel itt nem írhatunk függvény törzset ezért egy külön contract osztályt kell készíteni. Ezt az osztályt és az interfészt attribútumokkal kapcsoljuk össze.
[ContractClass(typeof(IFooContract))]
interface IFoo
{
int Count { get; }
void Put(int value );
}
[ContractClassFor(typeof(IFoo))]
sealed class IFooContract : IFoo
{
int IFoo.Count
{
get
{
Contract.Ensures( 0 <= Contract.Result() );
return default( int ); // dummy return
}
}
void IFoo.Put(int value)
{
Contract.Requires( 0 <= value );
}
}
Absztrakt metódus contract-ok
Az interfészekhez hasonlóan itt sem lehet függvény törzset írni, ezért ugyan úgy mint az előbb itt is egy külön osztályban kell leírni a contract-ot, amit attribútumokkal kapcsolunk össze az absztrakt metódussal.
[ContractClass(typeof(FooContract))]
abstract class Foo
{
public abstract int Count { get; }
public abstract void Put(int value );
}
[ContractClassFor(typeof(Foo))]
abstract class FooContract : Foo
{
public override int Count
{
get
{
Contract.Ensures( 0 <= Contract.Result() );
return default( int ); // dummy return
}
}
public override void Put(int value)
{
Contract.Requires( 0 <= value );
}
}
Contract metódusok túlterhelése
Mindegyik metódusnak lehet egy string típusú paramétere is. Ez kiíródik, ha a feltétel nem teljesül. A string értékének fordítási időben ismertnek kell lennie.
Contract.Requires( x ! = null, " If x is null , then the missiles are fired ! " );
Contract öröklődés
Egy contract a típus altípusára is öröklődik. Lényegében megegyezik a megszokott öröklődéssel egyedül az előfeltételeknél van különbség, mégpedig az, hogy az altípus előfeltételének gyengébbnek kell lennie ezért, ha az őstípusnál nincs megadva semmilyen előfeltétel, akkor az azt jelent, hogy az azonosan igaz az előfeltétele ezért az altípusokhoz nem lehet előfeltételt írni. Mivel az utófeltételnél erősebbet kell megadni az altípusnál ezért itt nincs ez a probléma.
Contract attribútumok
A következő attributumok kapcsolódnak a contract-okhoz.
ContractClass és ContractClassFor
Interfészeknél és absztrakt típusoknál a contract-ot külön osztályban kell megfogalmazni. A ContractClass attribútumot az interfészhez (vagy absztrakt típushoz) kell adni. Ez az attribútum a különálló contract-ot megvalósító osztályra mutat.
[ContractClass(typeof(ContractForJ))]
interface J { ... }
A ContractClassFor attribútumot pedig a contract-ot megvalósító osztálynál alkalmazzuk. Ez azt mutatja, hogy a contract melyik interfészhez vagy absztrakt típushoz tartozik.
[ContractClassFor(typeof(J ))]
class ContractForJ : J { ... }
ContractInvariantMethod
Ezzel az attribútummal jelöljük, hogy az adott metódust invariánsként szeretnénk használni. Ennek a metódusnak void típusúnak kell lennie és nem hivatkozhat olyan függvényre, ami szintén invariáns.
Pure
Ezt az attribútumot olyan metódusoknál és deklarációnál lehet használni, amiknek nincsen
mellékhatásuk. Contract-okban csak ilyen attribútummal jelölt metódusokat lehet alkalmazni.
Ha egy delegáltnál használjuk ezt az attribútumot, akkor az azt jeleni, hogy az összes
példánya mellékhatás mentes. Néhány létező delegáltat (mint például: System.Predicate
RuntimeContracts
Ez egy assembly szintű attribútum, ami azt jelzi, hogy egy assembly már felülíródott egy contrcat álltal.
ContractPublicPropertyName
Ezt az attribútumot azon mezőnél használják, ami egy contract metódusában szerepel, de a metódus láthatósága nagyobb minta e mezőé (pl.: privát mező és publikus metódus). Az attribútum segítségével ez nem jelent gondot.
[ContractPublicPropertyName("PublicProperty")]
private int internal;
public int PublicProperty { get { ... } }
Az attribútum paramétere egy string, ami az adott property neve. A mező típusa a propery típusára konvertálható kell, hogy legyen, amit jelenleg nincs ellenőrizve. Hiba keletkezik, ha a megadott nevű property nem létezik.
ContractVerification
Ezzel az attribútummal lehet jelezni, hogy az adott assembly-n, típuson vagy adattagon kell e végrehajtani ellenőrzést. A [ ContractVerification ( false )] attribútum azt jelenti, hogy a helyesség ellenőrzés nem hajtódik végre. Az ellenőrzést lehet engedélyezni egy típusra vagy assemblyre, ekkor a típus vagy assembly összes tagja ellenőrizve lesz, ha egy property-re van engedélyezve, akkor az összes getter setter függvénye validálva lesz.