SW wykład 11 - Slajd6
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
Mając dane sygnaturę i algebrę pierwotnego typu danych naszego języka, możemy już przedstawić definicję języka TINY dla tego pierwotnego typu danych. Nie wnikając zbytnio w szczegóły:
Zachowujemy składnię języka TINY, ale zamiast wyrażeń arytmetycznych przyjmujemy termy zbudowane ze zmiennych i z operacji danych w sygnaturze pierwotnego typu danych, a w miejsce nierówności w wyrażeniach logicznych wprowadzamy dowolne "aplikacje" nazw predykatów naszego pierwotnego typu danych do wyrażeń (termów tego typu).
Dziedziny semantyczne języka TINY definiujemy jak poprzednio, zmieniając jedynie definicję dziedziny stanów: są to teraz funkcje ze zbioru zmiennych w nośnik algebry (zbiór wartości pierwotnego typu danych).
W końcu, definicje funkcji semantycznych przenoszą się też niemal bez zmian: klauzule semantyczne pozostają identyczne, tyle tylko, że definiując znaczenie wyrażeń i formuł atomowych w wyrażeniach logicznych sięgamy po operacje i relacje dane w naszej algebrze pierwotnego typu danych języka.
Łatwo teraz widać, że początkowy język TINY to szczególny przypadek podanego tu uogólnienia, gdzie pierwotnym typem danych jest typ liczb całkowitych ze stałymi numerycznymi, operacjami dodawania, mnożenia i odejmowania i z predykatem nierówności.
