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 do 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 implementacji --- choć nie zawsze jest to konieczne, a dla wielu celów może być nieodpowiednie lub 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 punktem startu będzie poprawność częściowa, formułowana i dowodzona w logice, która w swej sformalizowanej wersji pochodzi od Tony'ego Hoare'a. Rozszerzana z jednej strony na coraz bardziej złożone konstrukcje programistyczne, z drugiej na mocniejsze własności poprawności (na przykład całkowitą poprawność 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 zastosowaniach metod formalnych w praktyce budowania oprogramowania wielką rolę odgrywają też metody budowania specyfikacji, opierające się na pojęciu modelu abstrakcyjnego.