Semantyka i weryfikacja programów/Ćwiczenia 3

Zadania z rozwiązaniami

Zadanie 1

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

$e\,::=\,\,\epsilon \,\,|\,\,e0\,\,|\,\,e1\,\,|\,\,e_{1}+e_{2}$

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

Rozwiązanie

Składnia wyrażeń pozwala na wygodny dostęp do najmniej znaczącego bitu liczby. Spróbujmy zatem zastosować metodę dodawania pisemnego:

$e_{1}0+e_{2}0\,\Longrightarrow \,(e_{1}+e_{2})0$ $e_{1}0+e_{2}1\,\Longrightarrow \,(e_{1}+e_{2})1$ $e_{1}1+e_{2}0\,\Longrightarrow \,(e_{1}+e_{2})1$

Ale co zrobić z przeniesieniem?

$e_{1}1+e_{2}1\,\Longrightarrow \,?$

Podstawowy pomysł to potraktować przeniesienie jak dodatkowy składnik:

$e_{1}1+e_{2}1\,\Longrightarrow \,((e_{1}+e_{2})+1)0$

Zauważmy, że w składni dopuszcza się dowolne przeplatanie operatora dodawania i bitów $0,1$. Tę dowolność wykorzystaliśmy właśnie w regułach powyżej. Gdyby nasz język ograniczyć tylko do składni

$e\,::=\,\,b\,\,|\,\,e_{1}+e_{2}$

$b\,::=\,\,\epsilon \,\,|\,\,b0\,\,|\,\,b1$

(nazwijmy ją składnią ograniczoną) to powyższe reguły byłyby niepoprawne.

Zanim dopiszemy pozostałe reguły, określmy zbiór konfiguracji jako zbiór wyrażeń. Konfiguracje końcowe to wyrażenia bez operatora dodawania (liczby binarne). Nasz pomysł jest taki, że tranzycje stopniowo przesuwają operator dodawania w lewo, aż się go ostatecznie pozbędą.

....