SW wykład 2 - Slajd19

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

Przystępujemy teraz do przedstawienie pierwszej, może najbardziej oczywistej przez jej związek z rzeczywistymi obliczeniami, metody opisu semantyki języków programowania. Dla instrukcji naszego przykładowego języka TINY podamy semantykę operacyjną w stylu określanym często jako semantyka małych kroków.

Na powyższym slajdzie przedstawiamy najbardziej zgrubnie jej najważniejsze pojęcia.

Jak będzie za chwilę widać na przykładzie, kluczowe jest tu pojęcie konfiguracji. O konfiguracjach należy myśleć jako o rzeczywistych konfiguracjach maszyny realizującej programy naszego języka. Oczywiście, na ogół konfiguracje abstrahują od pewnych szczegółów, które konfiguracje rzeczywistych maszyn muszą w sobie zawierać. W każdym razie, konfiguracje zawierać będą w jakiejś postaci zarówno sam realizowany program (a przynajmniej tę jego część, której realizacja nie została jeszcze zakończona), jak i pewną reprezentację stanu obliczeń maszyny.

Dla takich konfiguracji definiujemy relację przejścia: z grubsza, modelować ma ona pojedynczy krok maszyny realizującej programy. Obliczenie to po prostu ciąg kolejnych takich kroków, z których każdy następny rozpoczyna się w tej konfiguracji, do której doprowadził krok poprzedni. O obliczeniu, które rozpoczyna się od konfiguracji zawierającej pewną instrukcję, będziemy niekiedy mówić, że jest to obliczenie dla tej instrukcji, albo jeszcze krócej: obliczenie tej instrukcji.

Określimy też zbiór tych konfiguracji, które odpowiadają zakończeniu obliczeń programu.

Przyjmujemy przy tym, że dla każdego programu w danym języku programowania, wśród konfiguracji umieścimy konfigurację, która zawiera ten właśnie program jako "program do wykonania" w pewnym ustalonym otoczeniu początkowym. Wówczas zbiór możliwych obliczeń rozpoczynających się od takiej konfiguracji początkowej opisuje semantykę tego programu, a realizacja języka musi zapewnić, że rzeczywiste obliczenia maszyny dla tego programu odpowiadać będą obliczeniom opisanym przez semantykę.