SW wykład 7 - Slajd1

<<powrót do strony wykładu

Kontynuacje Kontynuacje wyrażeń i deklaracji Tiny+++ Dziedziny semantyczne Funkcje semantyczne Przykłady klauzul [[SW_wykład_7_-_Slajd7|Przykłady klauzul, c.d.] Instrukcje Bloki Skoki Semantyka skoków Semantyka skoków, c.d. Semantyka skoków, c.d. Semantyka skoków, c.d. Semantyka "standardowa"

Kończąc poprzedni wykład zasugerowaliśmy podstawową ideę, która prowadzi do kontynuacyjnego opisu semantyki języka programowania. Teraz pokażemy, jak ideę tę można zrealizować dla naszego języka TINY (ze wszelkimi rozpatrywanymi wyżej rozszerzeniami).

Posługiwać się będziemy pojęciem kontynuacji: kontynuacje przyporządkowują (bieżącym) stanom obliczeń (końcowe) odpowiedzi (czy też wyniki) programu. Formalnie zatem definiujemy dziedzinę kontynuacji jako dziedzinę funkcji ze stanów w odpowiedzi. Stany nie zawierają jednak już teraz wyjścia. Natomiast odpowiedzią (wynikiem obliczeń programu) jest właśnie potok wyjściowy (który może też kończyć się sygnałem błędu).

W ten sposób zdefiniowaliśmy dziedzinę kontynuacji dla instrukcji. Zgodnie z sugerowaną na poprzednim wykładzie intuicją, semantyka instrukcji w danym środowisku zmiennych i środowisku procedur określa przekształcenie kontynuacji (intuicyjnie: z punktu obliczeń bezpośrednio po wykonaniu danej instrukcji) w kontynuacje (intuicyjnie: z punktu obliczeń bezpośrednio przed wykonaniem danej instrukcji). Zatem znaczenia instrukcji to teraz funkcje z, kolejno, środowisk zmiennych, środowisk procedur, kontynuacji i stanu w odpowiedzi.