SW wykład 14 - Slajd6
Systematyczne konstruowanie programów Inżynieria wymagań Walidacja specyfikacji Strukturalne języki specyfikowania Zadanie programisty Uszczegóławianie Uszczegóławianie, c.d. Dekompozycja Wyzwanie
Tak jak omawialiśmy to na poprzednim wykładzie w odniesieniu do prostych instrukcji specyfikowanych przez parę warunków (wstępnego i końcowego), tak i tu: zadania programistycznego przedstawionego jako specyfikacja nie należy rozwiązywać metodą prób i błędów. Nawet jeśli przypadkiem doprowadzi ona do sukcesu (choć dla istotnie dużych i złożonych specyfikacji i systemów jest to jeszcze mniej prawdopodobne, niż dla prostych instrukcji rozważanych na poprzednim wykładzie) to będzie to proces bardzo długotrwały i kosztowny pod każdym względem.
Znacznie bardziej efektywnym podejściem jest stopniowe przekształcanie początkowej specyfikacji przez dodawanie do niej (czy uzupełnianie jej) o kolejne decyzje projektowe i programistyczne, dodatkowe własności, czy wręcz fragmenty kodu. Ważne jest jednak, by były to stosunkowo niewielkie i jasno przedstawione kroki, których weryfikacja będzie względnie prosta. Celem tego procesu jest osiągnięcie bardzo dokładnej specyfikacji, dla której wprost można podać realizację w wybranym języku programowania. Jeśli wykorzystywany język budowania specyfikacji to dopuszcza, specyfikacja ta po prostu może być dosłownie swoją realizacją (kodem systemu w języku programowania). Jeśli nie, to w "dobrych" językach budowania specyfikacji łatwo zidentyfikować podjęzyki, dla których przejście do kodu w języku programowania jest oczywiste. Na przykład, w klasycznym algebraicznym podejściu do specyfikacji systemów, specyfikacje budujemy jako listy równości mówiących o wymaganych związkach miedzy różnymi operacjami i stałymi udostępnianymi użytkownikowi przez specyfikowany system. Łatwo tu wyróżnić takie zbiory równości, które (zapewne z dokładnością do drobnych modyfikacji składniowych) po prostu są programami w językach programowania funkcyjnego.
Poprawność pojedynczych kroków przekształcenia specyfikacji orzekać można względem relacji uszczegóławiania między specyfikacjami, której formalna definicja oparta być musi o semantykę języka budowania specyfikacji. Niezbędnym wymaganiem, które taka definicja musi spełnić, jest by każdy program, który jest poprawną realizacją specyfikacji otrzymanej jako "wynik" ciągu przekształceń pewnej początkowej specyfikacji, był też poprawną realizacją tej początkowej specyfikacji. Przy standardowym podejściu do semantyki programów i ich specyfikacji, gdzie znaczeniem specyfikacji jest klasa struktur, znaczeniem programu jest struktura, a poprawność programu względem specyfikacji oznacza należenie struktury, będącej znaczeniem programu, do klasy struktur, będącej znaczeniem specyfikacji, odpowiednią relację uszczegóławiania specyfikacji określa po prostu relacja zawierania między klasami struktur będącymi znaczeniami tych specyfikacji (klasa struktur opisująca poprawne realizacje przekształconej specyfikacji ma być zawarta w klasie struktur opisującej poprawne realizacje specyfikacji przed przekształceniem). I znów, prostota tej definicji (i oczywiste spełnienie wymagania sformułowanego w ostatniej ramce na slajdzie) jest możliwa dzięki zapewne bardziej złożonej semantyce języka budowania specyfikacji i języka programowania.
