Semantyka i weryfikacja programów/Ćwiczenia 2

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania

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


Ćwiczenie 2

Rozszerzmy język Tiny o następujące dobrze znane konstrukcje iteracji:

Napisz semantykę małych kroków dla powyższych konstrukcji.


Rozwiązanie

Kalkulator binarny

Ćwiczenie 3

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

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


Rozwiązanie


Ćwiczenie 4

Rozszerzmy składnię o jeden symbol oznaczający "przepełnienie":

Na przykład oznacza tę samą liczbę, co , 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ń w składni ograniczonej:

reprezentujących sumę liczb binarnych.


Rozwiązanie

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 strategia lewo- albo prawostronna, ale niedozwolony jest "przeplot".


Ćwiczenie 3

Rozważ inną semantykę pętli , w której wyrażenie jest obliczane na nowo przed każdą iteracją pętli.


Ćwiczenie 4

Dodaj do wyrażeń binarnych operację odejmowania.


Ćwiczenie 5

Zaproponuj semantykę przypisania równoległego w języku TINY:

polegającego na obliczeniu najpierw wartości wyrażeń , a następnie na podstawieniu tych wartości na zmienne .