SW wykład 11 - Slajd11

<<powrót do strony wykładu

Poprawność systemu dowodzenia Hoare'a Dowód Dowód, c.d. Problem z pełnością Uogólnienie TINY${}_A$ TINY${}_A$ 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.