SW wykład 2 - Slajd22

<<powrót do strony wykładu

Składnia Składnia konkretna Składnia abstrakcyjna Przyjmowane założenia Przykład wiodący Kategorie składniowe Kategorie składniowe, c.d. Uwagi Indukcja strukturalna Definicje indukcyjne Kategorie semantyczne Wartościowanie zmiennych Semantyka wyrażeń Semantyka wyrażeń logicznych Semantyka instrukcji Prosty fakt Dowód Przezroczystość odwołań Semantyka operacyjna Obliczenia Semantyka operacyjna Tiny Własności Własności, c.d. Warianty definicji

Podana semantyka operacyjna instrukcji języka TINY pozwala na precyzyjne formułowanie i dowodzenie ich własności. Pierwszy prosty i bardzo podstawowy przykład to brak jakiegokolwiek niedeterminizmu: każda konfiguracja jest w relacji przejścia z nie więcej niż jedną konfiguracją. Dowód przez indukcję strukturalną po strukturze instrukcji jest naprawdę prosty (założenie indukcyjne wykorzystuje się jedynie dla sekwencyjnego złożenia instrukcji).

Ops! Sformułowanie kolejnego faktu na slajdzie jest nieprecyzyjne. Konsekwencją determinizmu języka jest jedyność maksymalnego obliczenia zaczynającego się w danej konfiguracji. Oczywiście, nie-maksymalnych obliczeń może być wiele. Łatwo pokazać jednak, że dla każdych dwóch obliczeń zaczynających się w tej samej konfiguracji, jedno z nich jest prefiksem drugiego.

Z pojęciem obliczenia wiąże sie oczywista, kolejna technika dowodów własności obliczeń (a więc pośrednio także własności programów): indukcja względem długości obliczenia.