Semantyka i weryfikacja programów/Ćwiczenia 10

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania

Funkcje

Zadanie 1

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

Deklaracja wprowadza funkcję o nazwie z jednym parametrem przekazywanym przez zmienną. Wykonanie funkcji polega na wykonaniu instrukcji , która powinna zawierać przypisanie na identyfikator . Takie przypisanie ustala wartość funkcji ale nie kończy wykonania instrukcji i.

Kontynuacje instrukcji

Zadanie 2

Powróćmy do języka TINY. Dodajmy do niego następujące instrukcje:

Zdefiniuj semantykę kontynuacyjną powyższych instrukcji. Możesz przy tym korzystać z gotowych już funkcji semantycznych dla pozostałych kategorii (w semantyce bezpośredniej) syntaktycznych.

Zadanie 3

Rozszerz język z poprzedniego zadania o konstrukcje


Zadanie 4

Uzupełnij definicję języka o bloki, deklaracje zmiennych i procedur oraz wywołanie procedury.

Zadanie 5

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

Program i instukcje postaci są blokami. Instrukcja break powoduje natychmiastowe wyjście z bloku i wznowienie wykonania od następnej instrukcji po bloku. Instrukcja again to skok do pierwszej instrukcji w najbardziej zagnieżdżonym bloku, w którym wystąpiła. Instrukcja rollback działa podobnie jak break, ale anuluje wszystkie zmiany dokonane od ostatniego wejścia do bloku, w którym wystąpiła.

Wykonanie programu:

 begin
   x := 2;
   begin
     x := x + 1;
     if x = 5 then rollback else again
   end
 end

zakończy się ze zmienną równą 2. Choć środowiska wydają się tu niepotrzebne, spróbuj wykorzystać je do przechowywania pewnych potrzebnych informacji.