SW wykład 1 - Slajd10
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ęć
Celem programisty zawsze powinno być zbudowanie nie tylko efektywnego i działającego, ale przede wszystkim poprawnego programu, który realizować będzie wcześniej określone zadania i cele (czy innymi słowy, spełniać będzie wymagane od niego własności). Dla stosunkowo małych zagadnień programistycznych może się tu sprawdzić metoda oparta w dużym stopniu na intuicji i praktyce programisty: otrzymujemy zadanie, rozumiemy je jako tako, siadamy i generujemy kod. (Szybko usuwamy proste błędy syntaktyczne, być może też testujemy na wszelki wypadek program na kilku prostych zestawach danych wejściowych). Teraz pozostaje już tylko udowodnić jego poprawność --- przy odrobinie szczęścia i wprawy, otrzymany program jest rzeczywiście poprawny i uda nam się tę poprawność wykazać, stosując odpowiedni system dowodzenia (dodajmy: nieważne jest przy tym w tym momencie, do jakiego stopnia sformalizowane są pożądane własności programu, które musimy zapewnić, i do jakiego stopnia sformalizowany jest system ich dowodzenia). Ale już dla programów bardziej złożonych (niż programy klasy "oblicz pierwiastek kwadratowy z liczby naturalnej" :-) szanse powodzenia dla postępujących tą drogą są minimalne. Na ogół zbyt wielka jest liczba szczegółów, by bez starannej ich analizy i systematycznego podejścia do budowania programu można było je wszystkie jednocześnie uwzględnić w trakcie konstrukcji programu, a potem niejako na nowo "odkryć" w procesie dowodzenia poprawności wcześniej zbudowanego programu. Tego typu kłopoty oczywiście znacząco rosną przy naprawdę dużych projektach, zatrudniających wiele zespołów programistycznych do realizacji różnych części danego programu, gdzie konstrukcja i dowodzenie własności programu i jego fragmentu w naturalny sposób zostają od siebie oddzielone nie tylko w czasie, ale i przez ich realizację przez różne grupy osób.
Z tych powodów, takiemu stylowi postępowania przeciwstawia się od lat jedynie słuszną drogę: budujmy programy od razu tak, by wraz z ich konstrukcją zapewniać ich poprawność, w dużym stopniu eliminując konieczność dowodzenia pożądanych własności programu niejako po omacku, gdy dany jest już gotowy program.
W tej metodzie postępowanie rozpoczynamy od ścisłej (najlepiej: formalnej) specyfikacji własności programu, które programista musi zapewnić. Następnie tę specyfikację wzbogacamy, krok po kroku dodając kolejne szczegóły, wprowadzając decyzje implementacyjne. Ważną klasę decyzji stanowić tu musi opracowanie modularnej struktury budowanego systemu oprogramowania i precyzyjne przedstawienie własności poszczególnych modułów, zależności między nimi i sposobu łączenia ich w cały, złożony system. Dopiero końcową i względnie prostą fazą jest kodowanie, polegające na prostej realizacji szczegółowo już opisanych własności modułów przez odpowiednie fragmenty programu.
Takie postępowanie zapewnia budowę programów spełniających pierwotnie sformułowane oczekiwania, gdzie sam proces konstrukcji składa się ze stosunkowo prostych i łatwych do zrozumienia uzasadnienia i weryfikacji kroków, a poprawność wyniku zapewnia poprawność całej metody. Okazuje się przy tym, że tak budowane programy niejako "za darmo" otrzymujemy z dobrą i pełną dokumentacją w postaci specyfikacji modułów stopniowo wprowadzanych w procesie konstrukcji programu. Są więc też one znacznie łatwiejsze do późniejszej analizy i modyfikacji.
