Semantyka i weryfikacja programów/Ćwiczenia 5

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania

Zawartość

Kontynuujemy ćwiczenie semantyki naturalnej, dodając pewne konstrukcje do języka TINY. W szczególności rozszerzymy go o deklaracje zmiennych (bloki). Po raz pierwszy roszdzielimy informację przechowywaną w konfiguracji na środowisko określające wiązanie identyfikatorów i stan przechowujący wartości zmiennych. Będzie to przygotowanie do kolejnych zajęć.


Semantyka naturalna pewnej instrukcji

Ćwiczenie 1


Rozszerzamy język TINY następująco:

Znaczenie instrukcji jest następujące. Obliczamy wartości wyrażeń i . Jeśli pierwsza z nich jest mniejsza od lub równa drugiej, podstawiamy pierwszą wartość (wartość wyrażenia ) na zmienną i uruchamiamy . Jeśli w nie zostanie napotkana instrukcja , kończymy instrukcję i przyracamy wartość zmiennej sprzed tej instrukcji. Natomiast jeśli w zostanie napotkana instrukcja , podstawiamy na kolejną, o jeden większą wartość, przywracamy wartości wszystkich pozostałych zmiennych sprzed instrukcji i ponownie wykonujemy . Powtarzamy w ten sposób, aż zakończy się nie napotkawszy , albo wartość zmiennej przekroczy wartość wyrażenia obliczoną na początku. W pierwszym przypadku kończymy instrukcję i przyracamy wartość zmiennej sprzed tej instrukcji. W drugim przywracamy wartości wszystkich zmiennych sprzed instrukcji i uruchamiamy .


Przykład

Oto przykładowy program:

x := 0; y := 1;
 x := 1  5 
  y := y+1;
   x <= 4  z:= x


Wartości zmiennych po zakończeniu programu to: .


Rozwiązanie

Semantyka naturalna bloków

Ćwiczenie 2 (bloki i deklaracje zmiennych)

Rozszerz semantykę języka TINY o deklarację zmiennej:

Zasięgiem zmiennej jest instrukcja , czyli wnętrze bloku, w którym jest zadeklarowana. Zakładamy zwykłe (statyczne) reguły widoczności, przesłaniania, itp.


Rozwiązanie

Zadania domowe

Ćwiczenie 1

Napisz semantykę naturalną dla następującego rozszerzenia języka TINY:

Instrukcja oznacza podniesienie wyjątku o nazwie . Instrukcja wykonuje . Jeśli podczas wykonania zostanie podniesiony wyjątek , i albo , to następuje przerwanie i sterowanie zostaje przeniesione do (następuje obsługa wyjątku). Jeśli zaś podczas wykonania zostanie podniesiony wyjątek oraz i , to obsługa wyjątku przekazana jest do najbliższej instrukcji otaczającej . Umawiamy się, że otacza i wszystkie instrukcje wewnątrz , ale nie otacza .


Ćwiczenie 2

Zaproponuj modyfikację semantyki, w której deklaracja jest wykonywana "równolegle", analogicznie do przypisania równoległego. Przy takiej semantyce kolejność poszczególnych deklaracji powinna być nieistotna.