Semantyka i weryfikacja programów/Ćwiczenia 12

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania

Semantyka kontynuacyjna

Zadanie 1

Zdefiniuj kontynuacyjną semantykę następującego języka:

Znaczenie wszystkich konstrukcji z wyjątkiem oraz jest standardowe.

Znaczenie instrukcji jest następujące: najpierw jeden raz jest obliczana wartość wyrażenia i podstawiana na zmienną . Potem w pętli robimy co następuje: jeśli , to wykonujemy w stanie sprzed instrukcji for (w szczególności wartość zmiennej na początku wykonywania powinna być przywrócona do tej sprzed wykonania instrukcji for) i przechodzimy do dalszej części programu. Natomiast jeśli , to jest wykonywana instrukcja . Jeśli w nie zostanie napotkana instrukcja fail, to przywracamy starą wartość zmiennej (tę sprzed wykonania instrukcji for) i przechodzimy do dalszej części programu. Jeśli jednak napotkamy fail, to przywracamy stan sprzed wykonania instrukcji for (zachowując oczywiście wartość zmiennej ), zwiększamy wartość zmiennej o 1 i powtarzamy procedurę opisaną powyżej.

Instrukcja fail poza instrukcją for powinna powodować natychmiastowe zakończenie wykonywania programu. Jeśli fail występuję po else, czyli w , to odnosi się ono do (być może nieistniejącej) zewnętrznej pętli for.

Zadanie 2

Oto pewien śmieszny język programowania:

Programy w tym języku mogą wykonywać się w dwie strony: od lewej do prawej oraz od prawej do lewej. Wykonanie rozpoczyna się od pierwszej instrukcji i przebiega od lewej do prawej. Instrukcja back powoduje zmianę kierunku wykonania. Instrukcja left i powoduje wykonanie i jeśli wykonanie przebiega od prawej do lewej, w przeciwnym razie jest to instrukcja pusta. Symetrycznie działa right. Napisz semantykę tego języka.