SW wykład 13 - Slajd10

<<powrót do strony wykładu

Zadanie programistyczne Pierwsze podejście Przykład Weryfikacja Przykład Możliwe przyczyny porażki Poprawiony program Przykład dowodu Drugie podejście Wyprowadzanie programu Wyprowadzanie programu, c.d. Wyprowadzanie programu, c.d. Wyprowadzanie programu, c.d. Wyprowadzanie programu, c.d. Wyprowadzanie programu, c.d. Własność stopu Własność stopu, c.d. Poprawność przez konstrukcję

W pierwszym kroku konstrukcji odpowiedniej instrukcji podejmujemy decyzję, że będzie ona zbudowana jako sekwencyjne złożenie dwóch instrukcji. Zauważmy mimochodem, że takie i podobne decyzje programistyczne musiały też być podejmowane w trakcie pisania programu metodą prób i błędów. Ich źródłem musi być wiedza, doświadczenie i umiejętności programisty. Możliwe są też decyzje błędne, które nie będą prowadziły do sukcesu.

Tu jednak, każdą taką decyzję programistyczną podejmować musimy świadomie i jasno uzupełniać ją wymaganiami, które ona wprowadza.

W tym przypadku, decyzja o budowie programu będącego sekwencyjnym złożeniem dwóch instrukcji implikuje, że jego poprawność będzie musiała być uzasadniona przez regułę dowodzenia całkowitej poprawności dla instrukcji złożonej. Niezbędna jest zatem asercja pośrednia (warunek końcowy dla pierwszej instrukcji składowej i zarazem warunek początkowy dla drugiej instrukcji składowej). Określenie tej asercji pośredniej to niezbędna część tego kroku konstruowania programu!

Pełny krok konstruowania programu zawarty jest w

Schemat budowanego programu umieszczonym w podwójnej ramce u góry slajdu zawiera więc pełny opis tego kroku konstrukcji. Oznacza to nie tylko decyzję o budowie całego programu jako sekwencyjnego złożenia dwóch instrukcji, ale też wyznacza warunki poprawności, które muszą spełniać te składowe. Ważne jest przy tym, że konstrukcja tych składowych może teraz przebiegać wzajemnie niezależnie. W bieżącym kroku konstrukcji zapewniamy bowiem, że jeśli tylko otrzymamy instrukcje spełniające warunki poprawności zadane dla tych dwóch składowych, to tworząc z nich instrukcję złożoną, zbudujemy program całkowicie poprawny względem pierwotnych warunków początkowego i końcowego: wynika to z reguły dowodzenia całkowitej poprawności dla instrukcji złożonej.

Podsumowując raz jeszcze: zdecydowaliśmy w tym kroku, że dla konstrukcji całego programu wykorzystamy dwie instrukcje składowe; dla tych składowych podaliśmy specyfikacje, względem których mają one być poprawne; pokazaliśmy, jak mając dane instrukcje składowe zbudujemy cały program; i udowodniliśmy, że jeśli tylko te instrukcje składowe są poprawne względem ich specyfikacji, to tak zbudowany z nich program też będzie poprawny względem pierwotnej specyfikacji.

Proces dalszego konstruowania rozwiązania rozgałęzia się zatem teraz na dwa podzadania: konstrukcję pierwszej i drugiej składowej, odpowiednio, spełniających ich specyfikacje.