Next: Omówienie uzyskanych wyników Up: autoref Previous: autoref
Tematyka badañ
Praca po¶wiêcona jest badaniu poprawno¶ci i pe³no¶ci systemów dowodzenia s³u¿±cych wyprowadzaniu w³asno¶ci specyfikacji strukturalnych oraz relacji u¶ci¶lania miêdzy specyfikacjami strukturalnymi. Systemy te maj± du¿e znaczenie praktyczne. Umiejêtno¶æ dowodzenia w³asno¶ci danej specyfikacji pozwala na formalne dowodzenie w³asno¶ci programów spe³niaj±cych (implementuj±cych) tê specyfikacjê. Natomiast umiejêtno¶æ dowodzenia relacji u¶ci¶lania, modeluj±cej wymagania elementarnych kroków w procesie implementacji danej specyfikacji (patrz [SW 83,ST 88,IFIP 99]), pozwala na formalne sprawdzenie poprawno¶ci poszczególnych kroków implementacji -- a wiêc i ca³ego tego procesu.
Formu³ujemy równie¿ warunki, które powinna spe³niaæ logika le¿±ca u podstaw specyfikacji, by zaproponowane systemy dowodzenia dla rozpatrywanych specyfikacji strukturalnych by³y poprawne i pe³ne. Badamy tak¿e, które ze znanych logik spe³niaj± te warunki. W szczególno¶ci pokazujemy, ¿e logika le¿±ca u podstaw du¿ego fragmentu formalizmu CASL (patrz [CASL 99]) spe³nia te warunki.
Nie wszystkie jednak logiki s± wystarczaj±co ,,silne'', by zapewniæ zachodzenie warunków niezbêdnych dla pe³no¶ci wspomnianych powy¿ej systemów dowodzenia. Mo¿emy mieæ wówczas do czynienia z sytuacj±, w której pomimo tego, ¿e dany os±d dotycz±cy w³asno¶ci specyfikacji b±d¼ relacji u¶ci¶lania miêdzy specyfikacjami jest prawdziwy w rozwa¿anym systemie dowodzenia, nie bêdziemy w stanie go w tym systemie udowodniæ. Z praktycznego punktu widzenia oznacza³oby to, ¿e przy u¿yciu takich ,,s³abych'' logik nie bêdziemy w stanie udowodniæ pewnych, byæ mo¿e istotnych, w³asno¶ci specyfikowanych programów czy poprawno¶ci poszczególnych kroków implementacji. Aby temu zaradziæ, przedstawimy warunki, przy których ,,s³aba'' logika mo¿e ,,po¿yczyæ'' system dowodzenia od logiki ,,silniejszej'', w której mo¿emy wyprowadziæ wszystkie prawdziwe os±dy zbudowane nad ,,s³absz±'' logik±.
Odrêbnym zagadnieniem, które rozpatrujemy w tej pracy, jest stworzenie podstaw teoretycznych do u¿ywania znanych, komputerowo wspomaganych systemów dowodzenia twierdzeñ do wyprowadzania os±dów dotycz±cych specyfikacji strukturalnych rozpatrywanych w tej pracy.
Next: Omówienie uzyskanych wyników Up: autoref Previous: autoref RHS Linux User
2000-06-24