SW wykład 2 - Slajd20

<<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

Warto przy tym zwrócić uwagę, że wprowadzając pojęcie obliczenia, nie założyliśmy nic o sposobie ich zakończenia (ani też że w ogóle obliczenia się kończą). Mamy zatem trzy istotnie różne sytuacje dla obliczeń maksymalnych (takich, których nie można już przedłużyć). Po pierwsze, najbardziej oczekiwana jest sytuacja, gdy ostatnia konfiguracja obliczenia jest konfiguracją końcową (w sensie definicji konfiguracji końcowych w semantyce). Po drugie, możemy mieć do czynienia z sytuacją zakleszczenia obliczeń: obliczenie doprowadziło do nie-końcowej konfiguracji, z której nie można już wykonać żadnego kroku (leży ona poza dziedziną relacji przejścia). I w końcu, możemy mieć do czynienia z obliczeniem nieskończonym (bez konfiguracji końcowej), co modeluje sytuację pętlenia się programu.

Wprowadzamy też standardową notację dla zwrotnego i przechodniego domknięcia relacji przejścia, opisującego relację osiągalności między konfiguracjami przez skończone obliczenia, oraz jej składowe, mówiące o osiągalności między konfiguracjami przez obliczenia o określonej długości.