Delphiben nincsenek kifejezetten helyességbizonyítást támogató eszközök. Ugyanakkor az Embarcadero új .NET fejlesztői megoldása, a Delphi Prism már lehetővé teszi a szerződés alapú programozást.
Design by Contract
A Design by Contract egy programozási filozófia, amely lehetőséget nyújt a fejlesztőknek, hogy különböző feltételeket definiáljanak, melyeknek a program
futása előtt teljesülniük kell. Ugyancsak lehetőség van állítások definiálására, melyeknek egy adott osztályon belül igaznak kell lenniük. Így a kód
áttekinthetőbb és tagoltabb lesz: a "contract" részbe kerülnek az állítások, melyeknek igaznak kell lenniük egy adott blokk végrehajtása előtt. Gyakran a
fejlesztőknek sok "biztonsági" kódot kell írniuk, hogy a program megfelelően fusson - a Design by Contract egyszerűbbé teszi ezt.
Például gyakran előfordul, hogy egy objektumreferenciát ellenőrizni szeretnénk, mielőtt használjuk. Ez többnyire egy "biztonsági" kódrészlet beszúrásával
jár, ami nem feltétlenül illik az adott blokkba. A Design by Contract lehetővé teszi, hogy a kívánt állítást egy külön blokkban definiáljuk, és az eredeti
blokkba azzal a bizonyossággal írjuk a kódot, hogy az állítás igaz.
Ezenkívül ha a fő kódblokk lefut, a Design by Contract biztosítja, hogy az állítás teljesül az eredményre. Például ha egy függvény visszatérési értéke egy
érvényes referencia, a fejlesztő definiálhat egy szerződést, mely szerint a függvény eredménye egy érvényes referencia, amely nem NIL.
A Design by Contract elv Bertrand Meyer nevéhez fűzödik, aki az Eiffel nyelvet ezen filozófia alapján tervezte.
A Delphi Prism támogatja a Design by Contract elvet a require és ensure záradékokkal metódusokon belül, és az invariants résszel
osztályokon belül.
Elő- és utófeltételek
Tekintsük a következő kódot:
procedure SomeClass.AddToStringBuilder(aStringBuilder: StringBuilder; aString: Text);
begin
if (aStringBuilder <> nil) and (aString <> '') then
begin
aStringBuilder.Append(aString);
end;
end;
Ez egy kimondottan egyszerű példa, a kód két ellenőrzést tartalmaz: biztosítja, hogy a StringBuilder paraméter nem NIL, és a string paraméter nem üres. A legtöbb fejlesztő sok hasonló kódot ír. Azonban ez a példa keveri a biztonsági, hibaellenőrző kódot az aktuális, végrehajtandó kóddal.
A Delphi Prism nyelvi elemet biztosít a hasonló kódok egyszerűbbé tételére. A require és ensure kulcsszavak lehetővé teszik a fejlesztőnek, hogy a biztonsági kódot elkülönítse a tényleges kódtól. A require egy előfeltételt definiál, amelynek igaznak kell lennie a kód végrehajtása előtt, az ensure pedig megadja az utófeltételt, amelynek a kód végrehajtása után kell teljesülnie.
Ez alapján a kód a következőképpen alakítható át:
procedure SomeClass.AddToStringBuilder(aStringBuilder: StringBuilder; aString: Text);
require
aStringBuilder <> nil;
aString <> '';
begin
// a fő kód ide kerül
ensure
aStringBuidler <> nil;
aStringBuilder.Length > 0;
end;
A Design by Contract lehetővé teszi, hogy a szerződéseket még az implementáció előtt megírjuk. Ebben az esetben a require záradék két Boolean állítást tartalmaz, melyeknek igaznak kell lenniük a blokk végrehajtása előtt - megkövetelve, hogy aStringBuilder egy érvényes referencia, és aString nem egy üres string. Tehát a require záradék garantálja, hogy a program megfelelően viselkedik - még a fő kódblokk végrehajtása előtt.
És miután a fő kódblokk lefutott, az ensure záradék biztosítja, hogy aStringBuilder továbbra is érvényes, és tartalmaz valamilyen szöveget. Így az ensure záradék garantálja, hogy a fő kódblokk megcsinál/nem csinál meg bizonyos dolgokat, amiket az alkalmazás megkövetel.
Ha a szerződés nem teljesül, assertion váltódik ki. A tesztelés és fejlesztés feladata biztosítani, hogy ilyen assertion sose történjen. Ha mégis történik, a kódot át kell írni, hogy a szerződés mindig teljesüljön.
A fejlesztő abban a tudatban írhatja a kódot, hogy a require záradék biztosítja a szerződés teljesülését, és assertion váltódik ki, ha a kód megsérti a szerződést. Ha a fejlesztés és tesztelés során olyan hibák fordulnak elő, amiket a szerződés nem definiál, egyszerűen bővíthetjük a szerződést, hogy biztosítsa a kód helyességét.
A require és ensure záradék szintaxisa lehetővé teszi annak megadását, hogy milyen hibaszöveg íródjon ki assertion esetén:
procedure SomeClass.AddToStringBuilder(aStringBuilder: StringBuilder; aString: string);
require
aStringBuilder <> nil: 'The aStringBuilder parameter cannot be nil';
aString <> '': 'The aString parameter must contain at least one character';
begin
aStringBuilder.Append(aString);
ensure
aStringBuilder <> nil: 'aStringBuilder should not be set to nil';
aStringBuilder.Length > 0: 'aStringBuilder should always have some text';
end;
Amikor assertion váltódik ki, a megfelelő üzenet jelenik meg magyarázatként.
Ha a szerződés bekerül a metódusba, a fejlesztő nyugodt lehet, hogy a kód csak akkor hajtódik végre, ha a szükséges feltételek teljesülnek. Mi történik akkor, ha nem teljesülnek?
Nézzük a következő kódot, amely az előbbi rutint használja:
method MainForm.button1_Click(sender: System.Object; e: System.EventArgs);
var
SB: StringBuilder;
begin
AddToStringBuilder(SB, 'This will violate the contract');
end;
A kód egy nullpointert ad át az AddToStringBuilder eljárásnak, ami megsérti a szerződést. Az eredmény egy Assertion kivétel:
A hibaüzenet a require záradékból benne van az Assert üzenetben. Egy hasonló üzenet lenne az eredmény, ha a kód egy üres stringet kapna aString paraméterként.
Ez a lehetőség főleg a fejlesztés és tesztelés során hasznos. Az assertion-ök többnyire ki vannak kapcsolva egy alkalmazás végrehajtása során. De a tesztelési és fejlesztési fázisban a szerződések azonnal visszajelzést szolgáltatnak a helytelen kód okozta hibákról.
Osztályinvariánsok
Egy másik lehetősége a Design by Contract-nek az osztályinvariánsok. Az osztályok rendszerint adatokat tartalmaznak, és néha az adatoknak bizonyos határokon belül
kell lenniük, vagy egyéb megszorításokat kell teljesíteniük. Az osztályinvariánsok lehetővé teszik a fejlesztőnek, hogy állításokat vagy megszorításokat
definiáljon, melyek nem sérülhetnek meg az osztálypéldány élete során.
Nézzük a következő egyszerű osztálydeklarációt:
type
TCustomerWithInvariants = class
private
FCustomerAge: Integer;
private invariants
FCustomerAge < 120;
public
constructor Create;
property CustomerName: string;
property CustomerAge: Integer read FCustomerAge write FCustomerAge;
end;
Ez az osztály az ügyfél nevét és életkorát tárolja. Ugyancsak van egy private invariants szekciója, mely szerint az ügyfél életkora kisebb, mint 120. Az invariánsok egyszerű Boolean kifejezések, melyek az osztályra nézve megkövetelt/tiltott állításokat definiálnak.
Ha egy invariánst deklaráltunk, az osztály ellenőrzi az állítás helyességét, és assertiont vált ki, ha az invariáns megsérül. Ez biztosítja, hogy az osztályok mindig a megfelelő állapotban maradjanak.
method MainForm.button3_Click(sender: System.Object; e: System.EventArgs);
var
Customer: TCustomerWithInvariants;
begin
Customer := TCustomerWithInvariants.Create;
Customer.CustomerAge := 554;
textBox1.Clear;
textBox1.Text := 'Customer Age: ' + Customer.CustomerAge.ToString;
end;
Ha a fenti kódot próbáljuk végrehajtani, egy Assertion kivétel váltódik ki, mert az ügyfél életkorát 554-re állítottuk. Az osztályinvariánsok hasonlóan működnek, mint a require és ensure záradékok: assertiont váltanak ki, ha az "ígéretek" nem teljesülnek. Lehetővé teszik, hogy definiáljuk és teszteljük az osztályokat, biztosítva, hogy nem tartalmaznak a követelményeket nem teljesítő adatokat.
Összegzés
A Design by Contract egy hatékony módszer áttekinthető és kevesebb hibát tartalmazó kódok írására. Azzal, hogy szerződéseket definiálunk metódusokhoz és osztályokhoz, a kód tisztább lesz, és biztosak lehetünk benne, hogy a környezet garantálja a szerződések betartását. Ez a nyelvi elem egy nagy előnye a Delphi Prismnek a többi népszerű .NET nyelvvel szemben.