SW wykład 14 - Slajd5
Systematyczne konstruowanie programów Inżynieria wymagań Walidacja specyfikacji Strukturalne języki specyfikowania Zadanie programisty Uszczegóławianie Uszczegóławianie, c.d. Dekompozycja Wyzwanie
Wprowadzone wyżej rozumienie specyfikacji umożliwia traktowanie ich jako prezentacji zadania programistycznego: zbuduj program (system, moduł), który poprawnie realizuje daną specyfikację. Ścisła definicja faktu "program poprawnie realizuje specyfikację" musi być oczywiście podana w terminach ścisłej semantyki języka budowania specyfikacji i ścisłej semantyki języka programowania. Pojęcie całkowitej poprawności prostych instrukcji względem ich specyfikacji zadanych jako pary warunków (wstępnego i końcowego), wykorzystywane na poprzednim wykładzie, to tylko jeden, bardzo prosty przykład tej sytuacji.
Jak sugerowaliśmy wcześniej, w bardziej realistycznych przypadkach, systemy czy ich moduły semantycznie opisywane będą jako struktury (algebry, struktury pierwszego rzędu, itp.). Podobnie, specyfikacje z kolei definiować będą mniej lub bardziej pośrednio klasy takich struktur. Pojęcie poprawności systemu względem specyfikacji jest wówczas już bardzo oczywiste: system jest poprawny względem specyfikacji, gdy struktura będąca jego znaczeniem jest elementem klasy struktur, będącej znaczeniem tej specyfikacji. Oczywiście, prostota tej definicji jest możliwa tylko dzięki przesunięciu akcentu na odpowiednią, na ogół skomplikowaną, definicję semantyki systemów i ich specyfikacji.
