SW wykład 1 - Slajd9

<<powrót do strony wykładu

Wstęp Literatura Programy Programy, sprzeczne oczekiwania WielkiCel Składnia Semantyka Pragmatyka Logika Metodyka Implementacja Formalna semantyka Przykład Przykład, c.d. Przykład, reguła dowodzenia Uzasadnianie poprawności Plan zajęć

Punktem wyjścia dla precyzyjnego opisu i dowodzenia ważnych własności budowanych programów musi być system logiczny dla opisu struktur danych, na których ten program ma operować -- albo jeszcze prościej, pierwotnych typów danych języka, wbudowanych w jego semantykę, takich jak liczby całkowite czy wartości logiczne. Często wystarcza tu standardowa logika pierwszego rzędu (choć warto ją wzbogacić na przykład o zasadę indukcji dla liczba naturalnych, jeśli potrafimy je wyodrębnić w typach danych języka). Warto już tu zwrócić uwagę, że dla wielu celów odpowiednie jest nieco abstrakcyjne potraktowanie typów liczbowych języka, z pominięciem ich rzeczywistej ograniczoności w konkretnej implementacjach --- choć nie zawsze jest to konieczne, a dla wielu celów może być nieodpowiednie, czy po prostu niebezpieczne.

W oparciu o tę logikę, budujemy systemy logiczne mówiące już o własnościach programów w danym języku programowania. Dla wielu standardowych języków programowania, tu z kolei punktem startu będzie poprawność częściowa, formułowana i dowodzona w logice, która w swej sformalizowanej wersji pochodzącej od Tony'ego Hoare'a. Rozszerzana dalej z jednej strony na bardziej i bardziej złożone konstrukcje programistyczne, a z drugiej, na mocniejsze własności poprawności (na przykład, całkowitą poprawność po programów, obejmującą także własność stopu). Tej tematyce poświęcamy kilka ostatnich modułów tych zajęć.

Warto jednak wiedzieć, że w praktyce formułowania i dowodzenia własności programów (nie mówiąc już o teoretycznych podstawach tej tematyki) wykorzystuje się znacznie szerszą gamę systemów logicznych. Wielką karierę, choćby przez związki z sukcesem weryfikacji modelowej, robią na przykład różne wersje logiki temporalnej. Ważne są też rozmaite inne logiki modalne, budowane wokół modalności wyrażających inne niż dopuszczane w logice pierwszego rzędu meta-własności. Dla budowy specyfikacji modułów oprogramowania często wykorzystuje się różne metody algebraiczne. W końcu, w zastosowaniach metod formalnych w praktyce budowania oprogramowania wielką rolę odgrywają też metody budowania specyfikacji oparte o pojęcie modelu abstrakcyjnego.