SW wykład 11 - Slajd11: Różnice pomiędzy wersjami
Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| Linia 2: | Linia 2: | ||
[[Grafika:sw1110.png|frame|center|]] | [[Grafika:sw1110.png|frame|center|]] | ||
Warto też jednak wiedzieć, że nie dla każdego języka programowania da | |||
się podać relatywnie pełny system dowodzenia częściowej poprawności | |||
względem warunków wstępnego i końcowego, pokazując kolejne reguły dla | |||
wprowadzanych konstrukcji językowych. Staje się to niemożliwe, gdy | |||
język jest na tyle skomplikowany, że problem stopu dla instrukcji tego | |||
języka przestaje być rozstrzygalny już dla bardzo prostych | |||
(skończonych) algebr pierwotnego typu danych. | |||
Aktualna wersja na dzień 17:14, 10 paź 2006
Poprawność systemu dowodzenia Hoare'a Dowód Dowód, c.d. Problem z pełnością Uogólnienie TINY TINY Ekspresywność Relatywna pełność logiki Hoare'a Rozszerzenia Ograniczenia
Warto też jednak wiedzieć, że nie dla każdego języka programowania da się podać relatywnie pełny system dowodzenia częściowej poprawności względem warunków wstępnego i końcowego, pokazując kolejne reguły dla wprowadzanych konstrukcji językowych. Staje się to niemożliwe, gdy język jest na tyle skomplikowany, że problem stopu dla instrukcji tego języka przestaje być rozstrzygalny już dla bardzo prostych (skończonych) algebr pierwotnego typu danych.
