SW wykład 13 - Slajd8

<<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ę

Podana w górnej ramce na slajdzie próba dowodu znów kończy się niepowodzeniem! Podane asercje nie wyznaczają dowodu całkowitej poprawności instrukcji względem warunków początkowego i końcowego: niezmiennik pętli wzmocniony o negację warunku wejścia do ciała pętli nie implikuje warunku końcowego. I znów nie wiemy, czy program nie jest poprawny, czy tylko nam nie udało się tego pokazać...

Tu akurat łatwo sprawdzić, że program jest poprawny, a pokazać to można nieco wzmacniając niezmiennik pętli (jak w owalnej ramce na slajdzie).

Tak czy inaczej, nie widać tu śladu systematycznej metody, która mogłaby choć trochę usprawnić konstruowanie poprawnych programów. Wręcz przeciwnie, taka metoda prób i błędów w praktyce musi prowadzić na manowce. Nawet jeśli uda się uniknąć pełnego niepowodzenia, to na ogół do sukcesu dojdziemy po licznych i kosztownych w praktyce kolejnych próbach konstruowania programu i uzasadnienia jego poprawności.