Semantyka i weryfikacja programów/Ćwiczenia 3

Zawarto¶æ

Koñczymy semantykê ma³ych kroków i rozpoczynamy semantykê naturaln± (du¿e kroki). Uzupe³nimy semantykê naturaln± jêzyka Tiny o semantykê naturaln± wyra¿eñ boolowskich i arytmetycznych oraz semantykê b³êdów wykonania. Wreszcie dodamy now± instrukcjê pêtli $\mathbf{𝐥}\mathbf{𝐨}\mathbf{𝐨}\mathbf{𝐩}$ pozwalaj±c± na niestrukturalne przerwanie lub wznowienie iteracji (instrukcje $\mathbf{𝐞}\mathbf{𝐱}\mathbf{𝐢}\mathbf{𝐭}$ i $\mathbf{𝐜}\mathbf{𝐨}\mathbf{𝐧}\mathbf{𝐭}\mathbf{𝐢}\mathbf{𝐧}\mathbf{𝐮}\mathbf{𝐞}$).

Rozszerzenia semantyki jêzyka Tiny

Ćwiczenie 1

Zdefiniuj znaczenie wyra¿eñ boolowskich i arytmetycznych w jêzyku Tiny, w stylu du¿ych kroków (semantyka naturalna).

Rozwiązanie

{{{3}}}

Ćwiczenie 2

Rozwa¿ dodatkowo operacjê dzielenia:

$e::=\dots |e_1/e_2$

i rozszerz semantykê z poprzedniego zadania. Dzielenie przez zero jest b³±dem i koñczy natychmiast wykonanie programu. Oprócz stanu wynikiem programu powinna byc informacja o b³êdzie, je¶li b³±d wyst±pi³.

Rozwiązanie

{{{3}}}

Ćwiczenie 3

Rozszerzmy jêzyk Tiny o nastêpuj±c± instrukcjê pêtli:

$I::=\mathbf{𝐥}\mathbf{𝐨}\mathbf{𝐨}\mathbf{𝐩}I|\mathbf{𝐞}\mathbf{𝐱}\mathbf{𝐢}\mathbf{𝐭}|\mathbf{𝐜}\mathbf{𝐨}\mathbf{𝐧}\mathbf{𝐭}\mathbf{𝐢}\mathbf{𝐧}\mathbf{𝐮}\mathbf{𝐞}$

$\mathbf{𝐥}\mathbf{𝐨}\mathbf{𝐨}\mathbf{𝐩}I$ to instrukcja pêtli, $I$ stanowi instrukcjê wewnêtrzn±. Instrukcja $\mathbf{𝐞}\mathbf{𝐱}\mathbf{𝐢}\mathbf{𝐭}$ wychodzi z nabli¿szej otaczaj±cej pêtli $\mathbf{𝐥}\mathbf{𝐨}\mathbf{𝐨}\mathbf{𝐩}$ i kontynuuje wykonanie programu od pierwszej instrukcji za t± pêtl±. Instrukcja $\mathbf{𝐜}\mathbf{𝐨}\mathbf{𝐧}\mathbf{𝐭}\mathbf{𝐢}\mathbf{𝐧}\mathbf{𝐮}\mathbf{𝐞}$ powraca na pocz±tek instrukcji wewnêtrznej najbli¿szej otaczaj±cej pêtli $\mathbf{𝐥}\mathbf{𝐨}\mathbf{𝐨}\mathbf{𝐩}$.

Pozwa¿ zarówno semantykê naturaln± jak i semantykê ma³ych kroków.

Rozwiązanie (semantyka naturalna)

{{{3}}}

Rozwiązanie (ma³e kroki)

{{{3}}}

Zadania domowe

Ćwiczenie 1

Zaproponuj semantykê ma³o-krokow± dla rozszerzeñ jêzyka Tiny, które studiowali¶my powy¿ej.

Ćwiczenie 2

Napisz semantyjê naturaln± dla nieznacznie rozszerzonej wersji instrukcji $\mathbf{𝐥}\mathbf{𝐨}\mathbf{𝐨}\mathbf{𝐩}$:

$I::=x:\mathbf{𝐥}\mathbf{𝐨}\mathbf{𝐨}\mathbf{𝐩}I|\mathbf{𝐞}\mathbf{𝐱}\mathbf{𝐢}\mathbf{𝐭}x|\mathbf{𝐜}\mathbf{𝐨}\mathbf{𝐧}\mathbf{𝐭}\mathbf{𝐢}\mathbf{𝐧}\mathbf{𝐮}\mathbf{𝐞}x$

Identyfikator $x$ pe³ni tutaj rolê etykiety zwi±zanej z instrukcj± $\mathbf{𝐥}\mathbf{𝐨}\mathbf{𝐨}\mathbf{𝐩}$, jest te¿ parametrem dwóch pozosta³ych instrukcji. $\mathbf{𝐞}\mathbf{𝐱}\mathbf{𝐢}\mathbf{𝐭}x$ koñczy teraz najbli¿sz± otaczaj±c± pêtlê $\mathbf{𝐥}\mathbf{𝐨}\mathbf{𝐨}\mathbf{𝐩}$ o etykiecie $x$. Podobnie $\mathbf{𝐜}\mathbf{𝐨}\mathbf{𝐧}\mathbf{𝐭}\mathbf{𝐢}\mathbf{𝐧}\mathbf{𝐮}\mathbf{𝐞}x$ wznawia najbli¿sz± otaczaj±c± pêtlê o etykiecie $x$.

Przykład

{{{3}}}

koñczy dzia³anie z warto¶ci± zmiennej $a=3$. Za pomoc± wciêæ okre¶lili¶my, do wnêtrza której pêtli $\mathbf{𝐥}\mathbf{𝐨}\mathbf{𝐨}\mathbf{𝐩}$ nale¿y ka¿da z trzech ostatnich instrukcji przypisania. Niejednoznaczno¶æ bierze siê oczywi¶cie st±d, ¿e pracujemy ze sk³adni± abstrakcyjn±. Sk³adnia konkretna zawiera³aby prawdopodobnie jak±¶ konstukcjê zamykaj±c± pêtlê $\mathbf{𝐥}\mathbf{𝐨}\mathbf{𝐨}\mathbf{𝐩}$, np. $\mathbf{𝐥}\mathbf{𝐨}\mathbf{𝐨}\mathbf{𝐩}I\mathbf{𝐞}\mathbf{𝐧}\mathbf{𝐝}\mathbf{𝐥}\mathbf{𝐨}\mathbf{𝐨}\mathbf{𝐩}$.

Ćwiczenie 3

Napisz semantykê naturaln± i ma³o-krokow± dla rozszerzenia jêzyka Tiny o wyra¿enia z efektami ubocznymi:

$e::=\dots |\mathbf{𝐝}\mathbf{𝐨}I\mathbf{𝐭}\mathbf{𝐡}\mathbf{𝐞}\mathbf{𝐧}e|x:=e|x++|\dots$

Obliczenie wyra¿enia $\mathbf{𝐝}\mathbf{𝐨}I\mathbf{𝐭}\mathbf{𝐡}\mathbf{𝐞}\mathbf{𝐧}e$ polega na wykonaniu $I$ a potem na obliczeniu $e$. Warto¶æ wyra¿enia $x:=e$ jest taka jak warto¶æ wyra¿enia $e$ a efektem ubocznym jest podstawienie tej warto¶ci na zmienn± $x$.