Next: Spis Literatury Up: Wnioskowanie o programach za Previous: Tre¶æ pracy
Zakoñczenie
W pracy postawili¶my sobie za zadanie podanie jednego, spójnego formalizmu, systemu dedukcyjnego dla wnioskowania o w³asno¶ciach programów dopuszczaj±cych stosowanie wska¼ników wielokrotnych, aliasów zmiennych, tablic, przydzia³u i zwalniania pamiêci. Wywi±zali¶my siê z tego zadania przedstawiaj±c pewne rozszerzenie logiki algorytmicznej. Do jêzyka tej logiki w³±czyli¶my pojêcie wska¼ników i rekordów, dodali¶my mo¿liwo¶æ manipulowania wska¼nikami na wzór jêzyka programowania C, w³±czyli¶my instrukcje deklaracji zmiennych, przydzia³u i zwolnienia pamiêci. Uniknêli¶my tym samym potrzeby t³umaczenia konstrukcji jêzyka programowania do jêzyka logiki, co zwykle mocno komplikuje powsta³e formu³y i czyni wnioskowanie nienaturalnym i trudnym do zrealizowania. Dla tak okre¶lonego jêzyka podali¶my system dedukcyjny, którego poprawno¶æ i pe³no¶æ zosta³a wykazana.
Przedstawili¶my zastosowanie zaproponowanej logiki do specyfikacji znanych struktur danych. C-AL dobrze nadaje siê do tego celu, powsta³e specyfikacje s± bardzo zwiêz³e a przez to i czytelne (choæ, zdajemy sobie sprawê, ¿e jest to bardzo subiektywny os±d). W tym wypadku zwiêz³o¶æ specyfikacji rzeczywi¶cie implikuje ich czytelno¶æ, poniewa¿ pos³ugujemy siê naturaln± relacj± na wska¼nikach - relacj± osi±galno¶ci, nie pos³ugujemy siê za¶ (podaj±c dla kontrastu) do¶æ abstrakcyjnymi, matematycznymi pojêciami takimi, jak np. punkt sta³y.
Nieco gorzej prezentuje siê mo¿liwo¶æ wnioskowania w zaproponowanym formali¼mie. Tak jak niemal w ka¿dym rachunku, formalny dowód niebanalnych w³asno¶ci jest zazwyczaj d³ugi i skomplikowany, tak jest te¿ i w przypadku logiki C-AL. Szkic dowodu podstawowej w³asno¶ci algorytmu wyszukiwania elementu w drzewie BST zaj±³ nam dwie strony. Jednak, jak mo¿na zauwa¿yæ, w dowodzie tym brakowa³o g³ównie wyprowadzeñ dla kilku ogólnych w³asno¶ci niezwi±zanych bezpo¶rednio z dowodzon± w³asno¶ci±. To daje nadziejê na to, ¿e je¶li powiêkszy siê liczba ju¿ udowodnionych w³asno¶ci konkretnych struktur danych oraz ogólnych faktów dotycz±cych tej logiki, to wnioskowanie w tym formali¼mie bêdzie znacznie u³atwione.
Niniejsz± pracê nale¿y traktowaæ jako wstêp do zbadania mo¿liwo¶ci
logiki algorytmicznej w zakresie wnioskowania o programach ze wska¼nikami.
Dlatego dalsze badania powinny koncentrowaæ siê na kilku tematach. Po
pierwsze, nale¿a³oby tworzyæ bazê specyfikacji podstawowych struktur danych
wykorzystywanych w algorytmice oraz bazê podstawowych faktów na temat tych
struktur, co pozwoli zbadaæ na dalszych przyk³adach przydatno¶æ logiki
C-AL. Po drugie, nale¿a³oby dowie¶æ faktów ogólnych dotycz±cych tej
logiki, wspomagaj±cych dowodzenie w tym systemie takich, jak na przyk³ad
zasady rz±dz±cej relacj± osi±galno¶ci, regu³y i zasady ,,przeci±gania''
kwantyfikatorów przez instrukcjê przypisania. Kolejnym zadaniem s±
rozszerzenia proponowanej logiki. Ciekawym tematem badawczym by³aby na pewno
próba wykorzystania którego¶ z komputerowych narzêdzi wspomagania wnioskowania,
do pomocy w wyprowadzaniu dowodów w naszej logice.
Next: Spis Literatury Up: Wnioskowanie o programach za Previous: Tre¶æ pracy Adam Balaban 2002-03-21