Semantyka i weryfikacja programów/Ćwiczenia 2

Zawartość

Ćwiczymy dalej semantykę małych kroków. Uzupełnimy semantykę języka Tiny o semantykę operacyjną wyrażeń boolowskich i arytmetycznych. Następnie rozszerzymy nasz język o róznorodne konstrukcje iteracji. Na koniec zdefiniujemy operacje arytmetyczne liczb binarnych.

Rozszerzenia semantyki języka Tiny

Ćwiczenie 1

Semantyka języka Tiny z wykładu używała funkcji semantycznych $B,E:State\to State$ dla określenia znaczenia wyrażeń boolowskich i arytmetycznych. Zdefiniuj znaczenie wyrażeń za pomocą semantyki operacyjnej, w stylu małych kroków.

Rozwiązanie

{{{3}}}

Ćwiczenie 2

Rozszerzmy język Tiny o następujące dobrze znane konstrukcje iteracji:

$I::=\mathbf{𝐫}\mathbf{𝐞}\mathbf{𝐩}\mathbf{𝐞}\mathbf{𝐚}\mathbf{𝐭}I\mathbf{𝐮}\mathbf{𝐧}\mathbf{𝐭}\mathbf{𝐢}\mathbf{𝐥}b|\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}x:=e_1\mathbf{𝐭}\mathbf{𝐨}{e}_2\mathbf{𝐝}\mathbf{𝐨}I|\mathbf{𝐝}\mathbf{𝐨}e\mathbf{𝐭}\mathbf{𝐢}\mathbf{𝐦}\mathbf{𝐞}\mathbf{𝐬}I|\mathbf{𝐝}\mathbf{𝐨}I\mathbf{𝐰}\mathbf{𝐡}\mathbf{𝐢}\mathbf{𝐥}\mathbf{𝐞}b$

Napisz semantykę małych kroków dla powyższych konstrukcji.

Rozwiązanie

{{{3}}}

Kalkulator binarny

Ćwiczenie 3

Rozważmy następujący język wyrażeń (liczby binarne z dodawaniem):

$e::=ϵ|e0|e1|e_1+e_2$

$ϵ$ oznacza słowo puste, czyli np. $ϵ1011$ oznacza binarną liczbę 1011. Napisz semantykę operacyjną obliczającą wartość wyrażeń.

Rozwiązanie

{{{3}}}

Ćwiczenie 4

Rozszerzmy składnię o jeden symbol $p$ oznaczający przepełnienie:

$e::=ϵ|p|e0|e1|e_1+e_2.$

Na przykład $p101$ oznacza tę samą liczbę co $ϵ101$, ale z dodatkową informacją, że podczas jej obliczania nastąpiło przepełnienie. Rozumiemy przez to sytuację, gdy wynik ma więcej cyfr niż każdy z argumentów. Cyfry zero z lewej strony (najbardziej znaczące) również uważamy za pełnoprawne cyfry, nie należy ich usuwać ani dodawać nowych.

Napisz semantykę operacyjną obliczającą wartość wyrażenia wraz z informacja o ewentualnym przepełnieniu. Wynik powinien byc poprawny przynajmniej dla wyrażeń $e$ w składni ograniczonej:

$e::=b|e_1+e_2$

$b::=ϵ|b0|b1.$

Rozwiązanie

{{{3}}}

Zadania domowe

Ćwiczenie 1

Podaj przykład wyrażenia boolowskiego, które nie policzy się ani przy użyciu strategii lewo- ani prawostronnej, a policzy się przy strategii równoległej.

Ćwiczenie 2

Zmodyfikuj semantykę wyrażeń następująco: dla każdego podwyrażenia niedeterministycznie wybierana jest albo strategia lewo- albo prawostronna, ale niedozwolony jest ,,przeplot".

Ćwiczenie 3

Rozważ inną semantykę pętli $\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}x=e_1\mathbf{𝐭}\mathbf{𝐨}{e}_2\mathbf{𝐝}\mathbf{𝐨}I$, w której wyrażenie $e_2$ jest obliczane na nowo przed każdą iteracją pętli. Napisz reguły semantyczne dla tej instrukcji, nie odwołując się do innych istrukcji pętli.

Ćwiczenie 4

Dodaj do wyrażeń binarnych operację odejmowania.

Ćwiczenie 5

Zaproponuj semantykę przypisania równoległego w języku Tiny:

$x_1:=e_1||\dots ||x_n:=e_n$

polegającego na obliczeniu najpierw wartości wyrażeń $e_1,\dots ,e_n$ a następnie na podstawieniu tych wartości na zmienne $x_1,\dots ,x_n$.