SW wykład 14 - Slajd1
Systematyczne konstruowanie programów Inżynieria wymagań Walidacja specyfikacji Strukturalne języki specyfikowania Zadanie programisty Uszczegóławianie Uszczegóławianie, c.d. Dekompozycja Wyzwanie
Na poprzednim wykładzie przedstawiliśmy dość szczegółowo (choć na bardzo prostym przykładzie) proces konstruowania programów całkowicie poprawnych względem ich pierwotnej specyfikacji zadanej jako para warunków, wstępnego i końcowego. Dotyczyło to w gruncie rzeczy bardzo prostych programów, specyfikowanych w bardzo prosty sposób. Jednak przedstawione idee są znacznie bardziej ogólne i stosują się także w znacznie bardziej złożonych sytuacjach, w szczególności wówczas, gdy konstruujemy naprawdę duże systemy, a specyfikacje dotyczą nie pojedynczych, prostych programów iteracyjnych, ale systemów czy ich modułów, działających z wieloma zbiorami danych i udostępniających użytkownikowi szereg operacji służących ich przetwarzaniu, czytaniu, wprowadzaniu, itp. O systemach takich można myśleć jako o wielorodzajowych strukturach (algebrach, strukturach pierwszego rzędu, itp) złożonych z wielu "nośników" (zbiorów danych), funkcji (operacji na tych danych) i predykatów (relacji na tych danych). Formalna semantyka systemów oprogramowania i ich modułów odwzorowuje je wówczas w takie właśnie (lub im podobne) struktury.
Oczywiście, specyfikacje takich systemów są znacznie bardziej złożone niż rozważane specyfikacje dla prostych programów iteracyjnych (budowane po prostu jako para warunków, wstępnego i końcowego, dotyczących odpowiednich stanów --- początkowego i końcowego --- programu). Ważne jest jednak, by i w takich złożonych sytuacjach stosować metody systematycznego konstruowania systemów wraz z dowodem ich poprawności względem zadanej specyfikacji. Nie będzie tu czasu na szczegółowe przedstawienie tych zagadnień --- ale spróbujemy je choć naszkicować.
