SW wykład 12 - Slajd16: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| Linia 2: | Linia 2: | ||
[[Grafika:sw1215.png|frame|center|]] | [[Grafika:sw1215.png|frame|center|]] | ||
Asercje oraz wyrażenia określające funkcje w zbiór z relacją dobrze | |||
ufundowaną niezbędne dla pokazania całkowitej poprawności instrukcji | |||
języka TINY będziemy wplatać w tekst programu podobnie jak to było dla | |||
asercji częściowej poprawności. I podobnie jak tam, podane asercje | |||
wyznaczają dowód całkowitej poprawności instrukcji względem podanych | |||
warunków wstępnego i końcowego. | |||
Jeden z oczywistych wariantów notacyjnych pokazujemy na slajdzie. | |||
Oczywiście, odwołujemy się tu do definicji zbioru wartości i relacji | |||
dobrze ufundowanej na nim zadanych poza programem. | |||
Aktualna wersja na dzień 22:10, 16 paź 2006
Zadanie programistyczne Przykład Problemy z logiką Hoare'a Poprawność całkowita Poprawność całkowita, c.d. Poprawność całkowita, c.d. Reguła dla pętli Poprawność systemu dowodzenia dla Tiny Pełność systemu dowodzenia dla Tiny Przykład Uogólnienie Poprawność i pełność Relacje dobrze ufundowane Dowodzenie poprawności całkowitej Przykład Przykład Kolejny problem Binarne warunki końcowe Warunki poprawności Reguły dowodzenia Reguły dowodzenia, c.d. Przykład Logika algorytmiczna System dowodzenia
Asercje oraz wyrażenia określające funkcje w zbiór z relacją dobrze ufundowaną niezbędne dla pokazania całkowitej poprawności instrukcji języka TINY będziemy wplatać w tekst programu podobnie jak to było dla asercji częściowej poprawności. I podobnie jak tam, podane asercje wyznaczają dowód całkowitej poprawności instrukcji względem podanych warunków wstępnego i końcowego.
Jeden z oczywistych wariantów notacyjnych pokazujemy na slajdzie. Oczywiście, odwołujemy się tu do definicji zbioru wartości i relacji dobrze ufundowanej na nim zadanych poza programem.
