SW wykład 2 - Slajd21

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

I oto nasz przykład: semantyka operacyjna małych kroków dla instrukcji języka TINY. Konfiguracje to albo pary: instrukcja, która jeszcze ma być wykonana oraz aktualny stan (wartościowanie zmiennych), albo konfiguracje końcowe, którymi są po prostu stany. Oczywiście, jest to tylko bardzo abstrakcyjny opis rzeczywistych konfiguracji maszyny, która mogłaby implementować instrukcje języka TINY. Jej konfiguracje zapewne zawierałyby te informacje w sposób bardziej skomplikowany i mogłyby nieść wiele informacji dodatkowych. Niemniej, powinno być intuicyjnie oczywiste, że oczekiwana implementacja języka rzeczywiście budowana byłaby wokół konfiguracji, które mniej lub bardziej pośrednio reprezentowałyby informację zawartą w zdefiniowanych tu abstrakcyjnie konfiguracjach.

Relację przejścia definiujemy przez podanie należących do niej par konfiguracji. Zgodnie z intuicyjnym rozumieniem instrukcji, systematycznie przedstawiamy tu kroki obliczeń dla konfiguracji zawierających instrukcji poszczególnych postaci. Oczywiście, powyższe warunki podają tak naprawdę schematyczne określenia zbiorów takich par, otrzymywanych przez wstawienia za występujące tu meta-zmienne konkretnych fraz składniowych odpowiednich kategorii (zmiennych, wyrażeń arytmetycznych, wyrażeń logicznych, czy instrukcji) lub wartości z odpowiednich dziedzin semantycznych (stany).

Łatwo sprawdzić, że podane tu warunki określają relację przejścia jednoznacznie: wątpliwości mogą budzić warunki dla sekwencyjnego złożenia instrukcji, gdzie należenie pary konfiguracji do tej relacji zależy od należenia do niej innej pary. Jednak zależności te nie prowadzą do niejednoznaczności. Formalny dowód, że nie prowadzi to do niejednoznaczności, można przeprowadzić na przykład przez indukcję strukturalną po strukturze instrukcji języka zawartych w rozważanych konfiguracjach.