Next: Tre¶æ pracy Up: Wnioskowanie o programach za Previous: Wnioskowanie o programach za
Wstêp
Oprogramowanie i techniki komputerowe nabieraj± dzi¶ bardzo du¿ego znaczenia.
Coraz powszechniejsze staje siê ich zastosowanie w wielu dziedzinach
przemys³owych. Jednocze¶nie za b³êdy w oprogramowaniu przychodzi nieraz
zap³aciæ olbrzymi± cenê, szczególnie, gdy bierzemy pod uwagê zastosowania
komputerów w systemach podwy¿szonego ryzyka (ang. safety critical), gdy
w grê wchodzi zdrowie i ¿ycie ludzkie.
Rol± in¿ynierii oprogramowania, w tym metod formalnych, jest zwiêkszenie niezawodno¶ci systemów informatycznych. Niniejsza praca dotyczy tego w³a¶nie zagadnienia. Aby mówiæ o poprawno¶ci programu, musimy mieæ specyfikacjê okre¶laj±c± wymagania, które dany program ma spe³niæ oraz formaln± semantykê samego programu. Nale¿y równie¿ podaæ przepis na sprawdzenie (weryfikacjê), czy program spe³nia swoj± specyfikacjê. Bardzo wiele systemów formalnych powsta³o na u¿ytek weryfikacji programów. Do najbardziej znanych nale¿±: logika Hoare'a [Hoa69] w olbrzymiej liczbie wersji i rozszerzeñ (por. [Cou90] oraz [Apt81,Apt84]), rachunek transformacji predykatów Dijkstry [Dij85] i jego odmiany (por. np. [Nel87]), czy wreszcie logika dynamiczna [Har84] z jej równie du¿± liczb± odmian (por. [KT90]). Jednak istniej±ce rachunki i logiki programów zwykle pomijaj± kwestiê wska¼ników lub traktuj± j± w sposób niewystarczaj±cy (poprzez zbyt s³ab± wyra¿alno¶æ jêzyka orazub zbyt prosty przyjêty model obliczeñ). K³óci siê to z praktyk± programistyczn±, poniewa¿ bardzo wiele znanych algorytmów korzysta ze wska¼nikowych struktur danych.
Teza pracy Postawili¶my sobie za zadanie wype³nienie pojawiaj±cej siê luki poprzez przedstawienie jednego, spójnego formalizmu i systemu dedukcyjnego - logiki (oznaczanej w dalszym ci±gu przez C-AL) dla klasy programów dopuszczaj±cych wiele z³o¿onych konstrukcji i operacji, takich jak:
- wska¼niki (w tym wska¼niki wielokrotne, czyli wska¼niki do wska¼ników),
- aliasy zmiennych,
- tablice i rekordy,
- przydzia³ i zwolnienie pamiêci.
W naszej pracy bêdziemy korzystaæ z dorobku logiki algorytmicznej, jednej z najstarszych logik programów. Formalizm ten zosta³ zaproponowany przez A. Salwickiego [Sal70]. Podstawowym zadaniem logiki algorytmicznej jest wnioskowanie o w³asno¶ciach programów, nie mniej si³a wyrazu logiki algorytmicznej jest dostateczna do definiowania wielu znanych struktur danych w sposób jednoznaczny (kategoryczny), co nie dotyczy szeregu innych formalizmów, takich jak np. logika klasyczna. System dedukcyjny logiki algorytmicznej jest systemem poprawnym i pe³nym. Cen± pe³no¶ci tego systemu jest tzw. infinitiarny system dedukcyjny logiki, tzn. dopuszczaj±cy regu³y o nieskoñczonej liczbie przes³anek. W zamian za to nie ma potrzeby wprowadzania pojêæ relatywnej lub te¿ arytmetycznej pe³no¶ci koniecznych dla logik Hoare'a i logik dynamicznych (por. [Coo78,Har79]).
Logika algorytmiczna zaprezentowana w pracach Banachowskiego [Ban77], Mirkowskiej i Salwickiego [MS87,MS92], jest okre¶lona dla do¶æ w±skiej klasy programów (tzn. o ubogim zestawie instrukcji, bo s± to tzw. while-programy z dodan± instrukcj± procedury i bloku). Naszym zadaniem bêdzie rozszerzenie tej logiki o wspomniane wy¿ej operacje i konstrukcje.
Tez± niniejszej pracy jest wiêc stwierdzenie, ¿e istnieje logika pozwalaj±ca na specyfikacjê i dowodzenie w³asno¶ci programów korzystaj±cych ze wska¼ników. System dowodowy tej logiki jest systemem pe³nym.
Klasa programów, które chcemy opisaæ, bazuje na sk³adni i semantyce jêzyka C, poniewa¿ w sposób bardzo elastyczny i jednocze¶nie zwiêz³y i konsekwentny operuje on wska¼nikami. Nie jest jednak naszym celem zdefiniowanie pe³nej semantyki jêzyka C (z takimi niuansami, jak rzutowanie typów i bogatym jêzykiem wyra¿eñ z efektami ubocznymi).
Na koniec tego wstêpu, chcieliby¶my podzieliæ siê jeszcze jedn± uwag±, dotycz±c± pojêcia adresu. W rzeczywisto¶ci nie zajmujemy siê w tej rozprawie jedynie ,,niskopoziomowymi'' aspektami jêzyków programowania, jakie stanowi± z pewno¶ci± wska¼niki. Adres jest bowiem niczym innym jak identyfikacj± obiektu, za¶ identyfikacja jako taka, jest kluczowym zagadnieniem nie tylko dla jêzyka C, ale dla wszystkich jêzyków imperatywnych (problem aliasingu) i wszystkich jêzyków obiektowych (problem to¿samo¶ci dwóch kopii obiektu). My jedynie komplikujemy ten problem jeszcze bardziej, umo¿liwiaj±c manipulowanie adresami (tak jak to siê dzieje np. w jêzyku C).
Referowana rozprawa zosta³a zrealizowana czê¶ciowo w ramach projektu badawczego KBN nr 8 T11C 015 15.
Next: Tre¶æ pracy Up: Wnioskowanie o programach za Previous: Wnioskowanie o programach za Adam Balaban 2002-03-21