Next: Zakoñczenie Up: Wnioskowanie o programach za Previous: Wstêp
Tre¶æ pracy
Poni¿ej przedstawimy tre¶æ poszczególnych rozdzia³ów pracy.Poniewa¿ w rozdziale 3 podajemy bardzo zwiêz³± - formaln± definicjê naszej logiki, wcze¶niej, w rozdziale 2, zamie¶cili¶my wprowadzenie w stosowan± notacjê, podstawowe pojêcia i terminy. Omówiamy tam w kolejno¶ci: postaæ zmiennych, model pamiêci (w tym definicjê aliasu zmiennej, relacji osi±galno¶ci), okre¶lono¶æ termów. Nastêpnie omawiamy instrukcjê przypisania, deklaracjê zmiennych, postaæ typów z³o¿onych i kwantyfikatorów.
Warto w tym miejscu zauwa¿yæ, jak wiele mo¿e zale¿eæ od przyjêtego modelu
pamiêci. Zauwa¿my, ¿e w najprostszym przypadku, gdyby przyj±æ, ¿e pamiêæ
zajmuje jeden ci±g³y obszar adresowy, prawdziwe musia³oby byæ stwierdzenie, ¿e
ka¿de dwa adresy 
s± odlegle jedynie o pewne przesuniêcie 
.
To stwierdzenie nie zawsze jest jednak prawdziwe w rzeczywisto¶ci (poprzez zastosowanie pamiêci wirtualnej, rejestrów segmentowych, itp.), a wiêc programy nie powinny z tego faktu korzystaæ bez potrzeby, chocia¿by ze wzglêdu na przeno¶no¶æ kodu programów. W opisywanym modelu pamiêci mogliby¶my jednak wykazywaæ prawdziwo¶æ tego faktu. Równie¿ standardowe rozwi±zanie problemu przydzia³u i zwolnienia pamiêci polegaj±ce na wprowadzeniu pewnej puli adresów, które mog± zmieniaæ swój status (przydzielony/wolny) nie jest pozbawione b³êdów. Wyobra¼my sobie np. program, który przy ca³kowicie zajêtej pamiêci zwalnia jedn± komórkê pamiêci wskazywan± przez wska¼nik p. W takiej sytuacji, po ponownej alokacji jednej komórki pamiêci na wska¼nik q (przy za³o¿eniu pe³no¶ci systemu dowodowego), mogliby¶my w tym modelu pamiêci udowodniæ, ¿e p=q (a wiêc, ¿e p jest nadal sensownym wska¼nikiem). Tymczasem dalsze u¿ywanie przez program wska¼nika p jest b³êdem (gdy np. nasz program dzia³a w ¶rodowisku wieloprogramowym). W naszym modelu pamiêci unikniemy tych pu³apek - jest to model w którym pamiêæ jest podzielona na segmenty, a operacja przydzia³u pamiêci przekazuje zawsze ¶wie¿y (nowy) segment.
Spo¶ród wielu pojêæ, relacji i operatorów, które wprowadzamy w tym rozdziale,
na szczególn± uwagê zas³uguj± dwa. Po pierwsze, wprowadzamy relacjê
osi±galno¶ci.
Przyk³adowo, relacja
osi±galno¶ci mo¿e okre¶laæ
¿e pewien element wystêpuje w danym drzewie, a dok³adniej, ¿e
istnieje ¶cie¿ka adresów od korzenia drzewa do tego elementu.
Po drugie, umo¿liwiamy
kwantyfikowanie po adresach wystêpuj±cych na ¶cie¿kach adresów
rozpoczynaj±cych siê w pewnym konkretnym adresie. Przyk³adowo, kwantyfikator
ogólny postaci:
oznacza, ¿e w grafie o wierzcho³ku
nie wystêpuje warto¶æ 
.
Dziêki tym dwu konstrukcjom jêzyk zaproponowanej przez nas logiki
ma du¿± moc wyra¿ania i jest bardzo zwiêz³y.
Jak ju¿ to by³o wspomniane, formaln± definicj± sk³adni i semantyki naszej
logiki rozpoczynamy rozdzia³ 3. Z rzeczy mniej standardowych, definiujemy
tam pojêcie interpretacji w³a¶ciwej, czyli takiej, która spe³nia okre¶lone
za³o¿enia dotycz±ce no¶ników dla pewnych rodzajów (w szczególno¶ci,
zastrzegamy sobie w ten sposób sensowno¶æ interpretacji, poniewa¿ nasz model
pamiêci korzysta w³a¶nie z tych ogólnie dostêpnych rodzajów). Definiujemy
wreszcie, ¿e modelem dowolnej formu³y musi byæ interpretacja w³a¶ciwa (to
za³o¿enie jest zawarte w definicji relacji bycia modelem).
W kolejnym podrozdziale dowodzimy ca³ego szeregu lematów dotycz±cych semantyki logiki. Wreszcie wprowadzamy system dowodowy w dwóch etapach. W pierwszym etapie wprowadzamy wszystkie aksjomaty oprócz tych, które dotycz± przydzia³u i zwalniania pamiêci oraz deklarcji zmiennych. W drugim etapie wprowadzamy owe brakuj±ce aksjomaty, korzystaj±c przy tym z ju¿ wprowadzonego systemu dowodowego. Nie jest to typowe rozwi±zanie, pozwoli³o ono jednak na uproszczenie aksjomatyzacji. Rozdzia³ koñczymy przyk³adami wnioskowania we wprowadzonym systemie dowodowym, oraz dowodem poprawno¶ci przyjêtego systemu wnioskowania. Jest rzecz± oczywist±, ¿e dowód poprawno¶ci w sposób istotny korzysta³, w naszym przypadku, z za³o¿enia dotycz±cego modeli (tzn. ¿e s± nimi interpretacje w³a¶ciwe).
W rozdziale 4 udowodnili¶my pe³no¶æ aksjomatyzacji zaproponowanej logiki. Schemat dowodu oparty o znan± metodê - konstrukcjê Algebry Lindenbauma i istnienie odpowiedniego Q-filtru - zaczerpnêli¶my z pracy G. Mirkowskiej i A. Salwickiego [MS87]. Tu, jednak, nie oby³o siê bez niespodzianek. Przede wszystkim nale¿a³o uporaæ siê z za³o¿eniem o interpretacjach w³a¶ciwych z poprzedniego rozdzia³u. Dowód pe³no¶ci korzystaj±cy ze wspomnianej metody jest standardowy, o ile tzw. interpretacja kanoniczna okre¶lona przez pewien Q-filtr oka¿e siê byæ modelem odpowiedniej teorii. Ale w naszym przypadku musieli¶my dodatkowo wykazaæ, ¿e interpretacja kanoniczna jest interpretacj± w³a¶ciw±. Aby to wykazaæ, dowód musia³ równie¿ przebiegaæ wieloetapowo, co sk³ada³o siê w du¿ej mierze na trudno¶æ dowodu o pe³no¶ci. Kolejnym niestandardowym elementem tego dowodu okaza³ siê byæ jego koñcowy fragment, w którym wykazujemy, ¿e interpretacja kanoniczna jest modelem. Prawdziwo¶æ formu³y w danej interpretacji, w naszym przypadku, nie zale¿y bowiem ju¿ tylko od warto¶ciowania zmiennych, ale równie¿ od stanu pamiêci, alokacji oraz ilo¶ci wolnej pamiêci.
W rozdziale 5 zaprezentowali¶my zastosowanie naszej logiki zarówno do specyfikowania pewnych znanych wska¼nikowych struktur danych, jak i do dowodzenia w³asno¶ci programów korzystaj±cych z tych struktur. Przy pomocy kilku zwiêz³ych definicji, bez trudu uda³o siê nam wyspecyfikowaæ takie struktury danych, jak: listy (bez i z cyklem), drzewa, drzewa BST i AVL. W tym rozdziale przeprowadzamy równie¿ szkic dowodu poprawno¶ci programu znajduj±cego element w drzewie BST.
Next: Zakoñczenie Up: Wnioskowanie o programach za Previous: Wstêp Adam Balaban 2002-03-21