Semantyka i weryfikacja programów/Ćwiczenia 1

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania

Zawartość

Tematem tych zajęć jest semantyka operacyjna wyrażeń (małe kroki).


Semantyka operacyjna wyrażeń

Ćwiczenie 1

Rozważmy bardzo prosty język wyrażeń, którego składnia opisana jest następującą gramatyką:

Wynikiem wyrażenienia warunkowego jest wartość wyrażenia , o ile wyrażenie oblicza się do wartości różnej od zera; w przeciwnym przypadku wynikiem jest wartość wyrażenia .

Zaproponuj semantykę operacyjną (małe kroki) dla tego języka.

Rozwiązanie


Ćwiczenie 2

Rozszerzmy język wyrażeń z poprzedniego zadania o jedną konstrukcję

Wyrażenie zawiera w sobie deklarację , która stanowi mechanizm wiązania identyfikatorów w naszym języku. Deklaracja wprowadza nową zmienną oraz przypisuje jej wartość. Wartość wyrażenia obliczamy następująco: najpierw oblicza się wartość , podstawia ją za zmienną , a następnie oblicza wyrażenie . Zakresem zmiennej jest wyrażenie , czyli wewnątrz można odwoływać się (wielokrotnie) do zmiennej ; Ogólniej, odwołania do zmiennej w wyrażeniu odnoszą się do "najbliższej" (najbardziej zagnieżdzonej) deklaracji tej zmiennej. Taki mechanizm wiązania identyfikatorów nazywamy wiązaniem statycznym. Przyjmujemy zwykłe (statyczne) reguły przesłaniania zmiennych, np. jeśli w występuje podwyrażenie , to deklaracja "przesłania" deklarację w wyrażeniu .

Zakładamy, że na początku wartości wszystkich zmiennych są nieokreślone, czyli zmienne są niezainicjowane, a odwołanie do niezainicjowanej zmiennej jest uważane za niepoprawne.


{{przyklad|||

Rozwiązanie

Zadania domowe

Ćwiczenie 1

Zapisz wariant 2 semantyki z poprzedniego zadania.


Ćwiczenie 2

Dotychczas wystąpienie błędu podczas obliczania wyrażenia, np. odwołanie do niezainicjowanej zmiennej, powodowało, że wyrażenie nie posiadało wartości (nie było ciągu tranzycji prowadzących do konfiguracji końcowej). Zmodyfikuj którąś z semantyk z poprzednich zadań tak, aby błąd był komunikowany jako jedna z konfiguracji końcowych. To znaczy: jeśli obliczenie wyrażenia w stanie jest niemożliwe bo wystąpił błąd, to


Ćwiczenie 3

Rozważ rozszerzenie języka wyrażeń o wyrażenia boolowskie:

Zaproponuj semantykę małych kroków dla tego języka. Rozważ różne strategie obliczania wyrażeń boolowskich, oraz podejście leniwe. Na przykład w strategii lewostronnej dla , gdy zostało obliczone do , w podejściu leniwym nie ma wogóle potrzeby obliczania .