"Design by Contract" makrók
A Nemerle programhelyességi eszközkészlete elsősorban a Bertrand Meyer által bevezetett "Design by Contract" módszertan elemeit támogatja. Hasonló lehetőségeket nyújtanak például az Eiffel, Chrome vagy a Spec# nyelvek - a Nemerle ez utóbbit veszi mintául.
A helyességi szintaxis használatához importálnunk kell a Nemerle.Assertions makrókönyvtárat:
using Nemerle.Assertions;
A módszertant támogató nyelveknek lehetőséget kell biztosítaniuk a program értékeire vonatkozó feltételek explicit specifikációjára, például:
- Előfeltételek: Olyan logikai kifejezések, melyeknek teljesülniük kell egy metódus hívása előtt. Általában a metódus paramétereire vonatkoznak, de bármilyen kifejezés lehet, amelyet a metódus hívásának pillanatában ki lehet értékelni.
- Utófeltételek: Az előfeltételhez hasonlóan az utófeltétel egy logikai kifejezés, melynek teljesülnie kell a metódushívás befejezésének pillanatában.
- Invariánsok: A program olyan tulajdonságai, melyek a futás során soha nem változnak meg. (Pl.: egy lista elemei mindig növekvő sorrendben rendezettek.)
- Egyéb megszorítások a program bizonyos részeire. (Pl.: Egy metódus nem változtatja meg az objektum állapotát.)
A Nemerle jelenleg még nem támogat mindent a felsorolt lehetőségek közül. Az alábbiakban ismertetjük a jelenleg elérhető eszközöket, valamint a tervezett további szolgáltatásokat.
Előfeltételek
Előfeltételeket a requires attribútum segítségével adhatunk meg. Egy egyszerű példa a használatra:
class String
{
public Substring (startIdx : int) : string
requires startIdx >= 0 && startIdx <= this.Length
{ ... }
}
Látható, hogy az attribútum használatával oly módon adhatunk meg előfeltételt, hogy az a metódus törzsét nem "szennyezi". A fordítóprogram automatikusan elhelyezi a metódus elején a kifejezés futási idejű ellenőrzését végző kódot. Ha az előfeltétel nem teljesül valamely hívás során, akkor egy AssertionException kivétel váltódik ki, melynek üzenete tartalmazza a sérült kifejezést.
A requires és a többi attribútum többször is szerepelhet egy metódus törzse előtt. Közvetlenül a paraméterlistába is beépíthetők, ezt mutatja az alábbi példa:
ConnectTrees (requires (!tree1.Cyclic ()) tree1 : Graph,
requires (!tree2.Cyclic ()) tree2 : Graph,
e : Edge) : Graph
{ ... }
Utófeltételek
Az előfeltételekhez hasonló módon adhatunk meg utófeltételeket is, ehhez az ensures attribútumot kell használnunk.
Ha az eljárás valamilyen értékkel tér vissza, az utófeltételben erre az értékre a value szimbólumon keresztül hivatkozhatunk.
Példa utófeltételek használatára:
class LinkedList
{
public Clear () : void
ensures this.IsEmpty
{ ... }
public Length () : int
ensures value >= 0
{ ... }
}
Osztályinvariánsok
Invariánsokat osztályokra definiálhatunk. Ehhez az invariant attribútumot kell használnunk az oszály definíciója előtt.
Egy példa:
class Vector [T]
invariant position >= 0 && position <= arr.Length
{
private mutable position : int = 0;
private arr : array [T] = array [];
public push_back (x : T) : void
{ ... }
Ily módon biztosíthatjuk, hogy az objektumaink állapota "érvényes", vagyis megfelel a definiált kikötéseknek.
Invariánsokkal kapcsolatban gyakran felmerülő probléma, hogy a feltételben szereplő változók egymás értékétől függenek, így gyakorlatilag egyiket sem tudjuk módosítani az invariáns sérülése nélkül. (Például: x == y + 5). Ezért szükség van egy tranzakciós mechanizmus bevezetésére, melynek segítségével az invariáns ideiglenes "kikapcsolható".
Erre ad lehetőséget az alábbi konstrukció:
expose (this) {
x += 3;
y += 3;
}
Az expose-nak azt az objektumot kell megadni, amelyre ideiglenesen ki szeretnénk kapcsolni az invariáns ellenőrzését.
Invariánsok ellenőrzése
Hatékonysági megfontolásokból az invariánsok ellenőrzése nem történik meg minden egyes értékadás vagy külső függvény hívása során. A Spec#-hoz hasonlóan erre ténylegesen csak az expose blokkok végén és public metódusok hívása után kerül sor.
Tervezett további lehetőségek
Az alábbi szolgáltatások még nem kerültek implementálásra, de remélhetőleg a közeljövőben elérhetőek lesznek:
- Az attribútumok öröklődése származtatott osztályokra. Például, ha egy interfész metódusaira elő- és utófeltételeket adunk meg, ezáltal előírhatjuk, hogy annak minden implementáció megfeleljen.
- Egy Spec#-hoz készített tételbizonyító eszköz beépítése. Lehetővé tenné, hogy bizonyos feltételek teljesülését nem csak futási időben, de fordítási időben is ellenőrizni lehessen.
- Az invariáns attribútum továbbfejlesztése, hogy jobban megközelítse a Spec#-os megfelelő funkcionalitását.