Semantyka i weryfikacja programów/Ćwiczenia 3: Różnice pomiędzy wersjami

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
 
Linia 74: Linia 74:
 
zbiór wyrażeń. Konfiguracje końcowe to wyrażenia bez operatora dodawania
 
zbiór wyrażeń. Konfiguracje końcowe to wyrażenia bez operatora dodawania
 
(liczby binarne). Nasz pomysł jest taki, że tranzycje stopniowo przesuwają
 
(liczby binarne). Nasz pomysł jest taki, że tranzycje stopniowo przesuwają
operator dodawania w lewo, aż się go ostatecznie ''pozbędą''.
+
operator dodawania w lewo, aż się go ostatecznie <pre>''pozbędą''</pre>.
  
  

Wersja z 12:10, 27 lip 2006


Ć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