Next: Teza pracy Up: Specyfikacja wska¼nikowych struktur danych Previous: Specyfikacja wska¼nikowych struktur danych
Wstêp
Obecnie, gdy technika komputerowa ogarnia coraz wiêksze sfery naszego ¿ycia, coraz wiêkszego znaczenia nabiera jako¶æ wytwarzanego oprogramowania. G³ówn± cech± decyduj±c± o jako¶ci oprogramowania jest jego niezawodno¶æ. Gorsza funkcjonalno¶æ oprogramowania mo¿e oznaczaæ wiêkszy nak³ad pracy u¿ytkownika. Mniejsz± efektywno¶æ mo¿na próbowaæ kompensowaæ wiêkszymi zasobami sprzêtowymi lub d³u¿szym czasem pracy. Jednak b³êdy w oprogramowaniu potrafi± przynie¶æ trudne do przewidzenia straty i to w najmniej spodziewanym miejscu i chwili -- nie tylko tam, gdzie nastêpstwa takiego b³êdu mog± byæ gro¼ne dla ¿ycia ludzkiego (ang. safety critical applications), ale i w zwyk³ym biurze. Dlatego te¿ b³êdy w oprogramowaniu stawiaj± pod znakiem zapytania jego warto¶æ.Niezawodno¶æ oprogramowania ma równie¿ istotne znaczenie dla kosztów jego wytwarzania. W przypadku du¿ych systemów programistycznych koszty usuwania b³êdów przekraczaj± wielokrotnie koszty przygotowania jego pierwszej implementacji. W takiej sytuacji zwiêkszenie niezawodno¶ci oprogramowania mo¿e przynie¶æ du¿o wiêksze oszczêdno¶ci ni¿ np. zwiêkszanie efektywno¶ci zespo³u programistycznego.
Drog± do uzyskania niezawodnego oprogramowania jest zapewnienie jego poprawno¶ci na wszystkich etapach wytwarzania. W sytuacji, gdy stopieñ komplikacji du¿ych programów jest niemo¿liwy do ogarniêcia przez jednego cz³owieka, a zespo³y programistyczne licz± wiele osób, nie ma miejsca na domys³y co do poprawno¶ci poszczególnych zadañ projektowych i programistycznych. Ka¿da czê¶æ programu powinna zostaæ zweryfikowana. Aby mówiæ o poprawno¶ci programu, musimy mieæ specyfikacjê okre¶laj±c± wymagania, które ów program ma spe³niaæ. Je¿eli zarówno specyfikacja jak i program s± formalnie okre¶lone, to mamy mo¿liwo¶æ formalnego zweryfikowania poprawno¶ci jednego wzglêdem drugiego. St±d te¿ wynika istotna rola formalnych specyfikacji w wytwórstwie niezawodnego oprogramowania.
Gdy porównamy stosowane techniki programistyczne oraz znane metody specyfikacji, mo¿emy zauwa¿yæ pewn± rozbie¿no¶æ. Efektywne algorytmy, por. np. [BDR96,CLR97,Wir99], bardzo czêsto wykorzystuj± wska¼nikowe struktury danych. Z drugiej strony metody specyfikacji programów pomijaj± kwestiê wska¼ników lub traktuj± j± w sposób niewystarczaj±cy. Znane s± próby opisywania wska¼ników, czêsto jednak pozwalaj± one jedynie na wyra¿anie w³asno¶ci struktur danych w logice pierwszego rzêdu. Podej¶cia takie maj± ograniczone zastosowanie. Zwa¿my, ¿e logika pierwszego rzêdu nie pozwala na wyra¿enie takich podstawowych w³asno¶ci, jak spójno¶æ grafu, czy istnienie ¶cie¿ki o zadanych koñcach. Dlatego te¿ nie mo¿na za jej pomoc± opisaæ nawet tak podstawowej struktury danych, jak listy jednokierunkowe.
W niniejszej pracy prze¶ledzimy problem specyfikacji i weryfikacji wska¼nikowych struktur danych i programów na nich operuj±cych. Nasze rozwa¿ania s± osadzone w ramach metody zwanej podej¶ciem funkcyjnym (ang. functional approach) lub te¿ modelem czterech zmiennych Parnasa-Madeya (ang. Parnas-Madey Four Variable Model), przedstawionym w [PM95].
W podej¶ciu funkcyjnym w trakcie procesu wytwarzania programu powstaje szereg dokumentów opisuj±cych ten program na ró¿nych poziomach abstrakcji. W szczególno¶ci ka¿dy z modu³ów tworz±cych program jest opisywany na trzech poziomach szczegó³owo¶ci. S± to: specyfikacja interfejsu, projekt implementacji oraz implementacja modu³u. Dla naszych rozwa¿añ szczególnie istotne s±: projekt implementacji i implementacja. Tylko te dwa dokumenty dotycz± wska¼nikowych struktur danych stosowanych w programie. Projekt implementacji opisuje sposób implementacji struktury danych. Nie okre¶la on jednak sposobu implementacji operacji udostêpnianych przez modu³, a jedynie specyfikuje, w jaki sposób operacje te modyfikuj± strukturê danych modu³u. Implementacja modu³u jest zapisana ca³kowicie w jêzyku programowania.
Subsections
Next: Teza pracy Up: Specyfikacja wska¼nikowych struktur danych Previous: Specyfikacja wska¼nikowych struktur danych Marcin Kubica 2000-03-14