SW wykład 14 - Slajd3
Systematyczne konstruowanie programów Inżynieria wymagań Walidacja specyfikacji Strukturalne języki specyfikowania Zadanie programisty Uszczegóławianie Uszczegóławianie, c.d. Dekompozycja Wyzwanie
Wśród formalnych metod specyfikacji dużych systemów można, bardzo z grubsza, wyróżnić dwie klasy.
Pierwsza to specyfikacje oparte o przedstawienie konkretnego modelu systemu --- wykorzystujące rozmaite metody definiowania modeli, odpowiednie dla rozważanej klasy zastosowań. Mając taką specyfikację, system uznamy za poprawną jej realizację, jeśli obserwowalne przez użytkownika zachowanie tego systemu jest zgodne z odpowiednim zachowaniem modelu zawartego w specyfikacji.
Druga klasa to specyfikacje oparte o własności systemu. Tutaj jako specyfikację podajemy pewną listę własności oczekiwanych od systemu --- oczywiście, ta lista na ogół zostanie podana w jakiś strukturalny, bardziej czytelny sposób. I dalej, własności te sformalizowane mogą być jako formuły całej gamy systemów logicznych, odpowiednich dla danej dziedziny zastosowań. Mając taką specyfikację, system uznamy za poprawną jej realizację, gdy spełnia on wszystkie zawarte w tej specyfikacji własności.
Bez względu na to, w jaki sposób przedstawiona zostanie specyfikacja, ważnym problemem jest jej walidacja: stwierdzenie, czy zdołała ona uchwycić te wszystkie własności systemu, na których nam zależy. Tradycyjna metoda sprawdzania tego faktu to budowa prototypowego systemu realizującego mniej lub bardziej efektywnie daną specyfikację. Możemy wówczas taką prototypową realizację systemu testować, sprawdzając, czy wszelkie oczekiwane własności zostały zapewnione. Niekiedy jest to rzeczywiście rozsądna droga do oceny "jakości" specyfikacji, przynajmniej w pewnym zakresie. Zwróćmy jednak uwagę, że wybrana prototypowa realizacja systemu może spełniać pewne przypadkowe własności, które nie wynikają z samej specyfikacji, a są efektem wyborów dokonywanych w trakcie budowy "prototypu". Mogą one jednak być inne, niż decyzje podejmowane przy budowie ostatecznej wersji systemu. Niewiele więc takie testowanie w gruncie rzeczy zapewnia.
Znacznie bardziej "uniwersalną" metodą "testowania" specyfikacji jest precyzyjne formułowanie oczekiwanych własności sytemu i próba przeprowadzenia dowodu, że kolejne takie własności są formalnymi konsekwencjami zbudowanej specyfikacji. Dowody takie oczywiście muszą być oparte o formalną definicję semantyki specyfikacji i o ścisłe, dobrze zdefiniowane pojęcie konsekwencji specyfikacji.
