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$.