SW wykład 2 - Slajd24

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

Oczywiście, podana uprzednio definicja relacji przejścia nie jest jedyną zgodną z naszymi (nieprecyzyjnymi przecież) intuicjami o obliczeniach instrukcji w języku TINY. Na przykład, reguły dla konfiguracji zawierających instrukcje warunkowe przyjmują niejako, że wyliczenia warunku (wyrażenia logicznego) i sprawdzenia otrzymanej wartości logicznej odpowiadają jednemu krokowi obliczenia. Można semantykę napisać inaczej, na przykład rozbijając ten krok na dwa (obliczenie wartości wyrażenia logicznego w jednym kroku, sprawdzenie w drugim, czy jest to prawda, czy fałsz). Można też, jak wspominaliśmy wcześniej, podać prawdziwie operacyjną semantykę także dla wyrażeń arytmetycznych i logicznych, a następnie wykorzystać ją tutaj, wprowadzając obliczenia wartości wyrażeń logicznych jako część obliczeń semantyki operacyjnej instrukcji.

Kolejna możliwość, opisana na slajdzie, zawiera decyzję, że wyliczenia wartości wyrażeń i sprawdzenie ich wartości nie zajmują żadnego kroku obliczeń; relacja przejścia zawiera wówczas od razu kroki odpowiadające obliczaniu odpowiedniej gałęzi instrukcji warunkowej. Podobne rozważania można snuć dla instrukcji pętli, podając odpowiednie modyfikacje definicji relacji przejścia. Dochodzi tu jeszcze jedna oczywista możliwość: rozwinięcie w jednym kroku pętli do odpowiadającej jej instrukcji warunkowej (ponownie tę pętlę zawierającą w jednej z gałęzi).

Formalnie każda w tych możliwości prowadzi do innej semantyki operacyjnej instrukcji języka TINY. Na przykład, różne będą własności instrukcji związane z długością ich obliczeń. Można jednak łatwo sprawdzić, że przy każdym z naszkicowanych wyżej wariantów semantyki operacyjnej dla instrukcji języka TINY, obliczenia rozpoczynające się od tej samej konfiguracji prowadzą do tych samych konfiguracji końcowych.