Next: Podsumowanie Up: Specyfikacja wska¼nikowych struktur danych Previous: Teza pracy
Zawarto¶æ pracy
Poni¿ej przedstawiamy tre¶æ poszczególnych rozdzia³ów pracy.W rozdziale drugim znajduje siê wprowadzenie do podej¶cia funkcyjnego. We wprowadzeniu tym staramy siê abstrahowaæ od konkretnych metod specyfikacji, jakie s± zwykle wykorzystywane w ramach podej¶cia funkcyjnego. Koncentrujemy siê natomiast na roli poszczególnych dokumentów, ich ramowej postaci oraz informacjach, które powinny one zawieraæ. Szczególn± uwagê po¶wiêcamy projektowi implementacji. W rozdziale tym podajemy te¿, w jaki sposób mo¿emy modelowaæ za pomoc± wielosortowych algebr czê¶ciowych stany i modyfikacje wska¼nikowych struktur danych opisanych w projekcie implementacji. Rozdzia³ ten jasno okre¶la ramy, w jakich nale¿y osadziæ formalizm s³u¿±cy do specyfikowania wska¼nikowych struktur danych, pozostawiaj±c jednocze¶nie otwart± kwestiê wyboru takiego formalizmu.
Rozdzia³ trzeci zawiera krótkie wprowadzenia do kilku formalizmów, z których korzystamy w dalszej czê¶ci pracy. S± to: logika monadyczna drugiego rzêdu, logika sta³opunktowa, hipergrafowe gramatyki podmiany hiperkrawêdzi oraz wersja logiki modalnej s³u¿±cej do specyfikowania algebr dynamicznych [CR97] dostosowana do potrzeb tej pracy.
W rozdziale czwartym badamy przydatno¶æ ró¿nych formalizmów (w tym formalizmów przedstawionych w rozdziale trzecim) do specyfikowania wska¼nikowych struktur danych. Proponujemy te¿ w³asn± logikê s³u¿±c± do tego celu, zwan± logik± wielo¶cie¿kow±. Opieramy siê na specyfikacjach wybranych wska¼nikowych struktur danych zapisanych w poszczególnych formalizmach. W przypadku, gdy wyspecyfikowanie której¶ ze struktur danych w którym¶ formalizmie nie jest mo¿liwe, dowodzimy tego faktu. Porównuj±c badane formalizmy kierujemy siê dwoma kryteriami: ich si³± wyrazu oraz zwiêz³o¶ci± i czytelno¶ci± przyk³adowych specyfikacji. Struktur± danych wymagaj±c± najwiêkszej si³y wyrazu okaza³y siê drzewa AVL -- spo¶ród badanych formalizmów mo¿na je wyspecyfikowaæ jedynie za pomoc± logiki sta³opunktowej, logiki drugiego rzêdu i logiki wielo¶cie¿kowej. Niestety ¿aden z badanych formalizmów nie jest w pe³ni zadawalaj±cy pod wzglêdem czytelno¶ci specyfikacji. Jednak przeprowadzone porównanie jasno wskazuje, ¿e logika wielo¶cie¿kowa pozwala na najbardziej zwiêz³e i czytelne specyfikowanie wska¼nikowych struktur danych.
W rozdziale pi±tym zajmujemy siê problematyk± weryfikacji programów operuj±cych na wska¼nikowych strukturach danych. Jako przyk³adow± metodê weryfikacji przyjmujemy logikê Hoare'a. Zak³adamy przy tym, ¿e asercje s± wyra¿one w logice wielo¶cie¿kowej. Nale¿y jednak nadmieniæ, ¿e prezentowane wyniki nie ulegaj± zmianie, gdy logikê wielo¶cie¿kow± zast±pimy inn± logik± zawieraj±c± w sobie wszystkie konstrukcje logiki pierwszego rzêdu. Przedstawiamy wariant logiki Hoare'a dostosowany do weryfikacji while-programów operuj±cych na wska¼nikowych strukturach danych wzglêdem asercji wyra¿onych w logice wielo¶cie¿kowej, wraz z systemem dowodzenia. Pokazujemy, ¿e system ten jest poprawny oraz pe³ny w sensie Cook'a. Prezentowany formalizm jest zilustrowany za pomoc± przyk³adowej weryfikacji prostego programu.
Next: Podsumowanie Up: Specyfikacja wska¼nikowych struktur danych Previous: Teza pracy Marcin Kubica 2000-03-14