Semantyka i weryfikacja programów/Ćwiczenia 3

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania


Ćwiczenia 3: Dodawanie binarne (małe kroki)

Zadania z rozwiązaniami

Zadanie 1

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

oznacza słowo puste, czyli np. 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:

Ale co zrobić z przeniesieniem?

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

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

(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ą''

.


....


Zadanie 2