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ą dla wyrażeń boolowskich i arytmetycznych i semantykę dla błędów wykonania. Wreszcie dodamy instrukcję pętli i instrukcje niestrukturalnego zakończenia pętli (instrukcje i ).
Rozszerzenia semantyki języka Tiny
Zadanie 1
Zdefiniuj znaczenie wyrażeń boolowskich i arytmetycznych w języku Tiny, w stylu dużych kroków (semantyka naturalna).
Rozwiązanie
Przypomnijmy składnię wyrażeń boolowskich i arytmetycznych jezyka Tiny:
Chcemy, aby tranzycje wyrażen wyglądały następująco:
gdzie , jest liczbą całkowitą, , a . Tranzycja taka oznacza, że wyrażenie w stanie wylicza się do wartości oraz analogicznie, wyrażenie logiczne w stanie wylicza się do . Zatem zbiór konfiguracji dla semantyki całego języka Tiny to znów
a konfiguracje końcowe to tak jak poprzednio. Tranzycje dla instrukcji pozostają zasadniczo bez zmian, z tym, że odwołania do funkcji semantycznych dla wyrażen zastępujemy przez odpowiednie tranzycje. Np. dla instrukcji pętli będziemy mieć następujące reguły:
Podobnie dla instrukcji warunkowej. Teraz zajmiemy się tranzycjami dla wyrażeń. Zacznijmy od stalych arytmetycznych i boolowskich:
Operatory arytmetyczne definiujemy następująco:
Czyli aby obliczyć sumę w stanie , trzeba najpierw obliczyć i w tym stanie, a następnie dodać obliczone wartości. Zauważmy, że nie specyfikujemy kolejności, w jakiej mają się obliczać obydwa podwyrażenia. I choć tutaj nie ma to żadnego znaczenia, w przyszłości będzie inaczej, gdy jezyk będzie umożliwiał efekty uboczne podczas obliczania wyrażeń.
Podobne reguły można napisać dla pozostałych operacji arytmnetycznych, oraz dla spójników logicznych:
Oto inny wariant, reguły lewo-stronne (ponieważ rozpoczynamy od lewego koniunktu):
Inny wariant to wariant prawo-stronny ( najpierw , potem ). Wreszcie rozważmy kombinację obydwu semantyk (reguły równoległe):
Czyli jeśli którekolwiek z podwyrażeń daje wynik , to taki wynik zyskuje całe wyrażenie. Dodatkowo potrzebujemy jeszcze reguły:
W naszym prostym języku wszystkie cztery warianty są równoważne. Reguły dla pozostałych spójników logicznych, dla negacji oraz dla instrukcji przypisania pozostawiamy jako proste ćwiczenie.
Zadanie 2
Rozważ dodatkowo operację dzielenia:
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 (szkic)
Dopóki nie wystąpi błąd dzielenia przez zero, semantyka programu powinna być identyczna jak w poprzednim zadaniu. Zatem pozostawiamy wszystkie reguły z poprzedniego zadania. Dodatkowo potrzebujemy reguł, które opiszą
- kiedy powstaje błąd oraz
- jak zachowuje się program po wystąpieniu błędu
Zaczynamy od pierwszego punktu. W tym celu dodajemy do konfiguracji jedną konfigurację końcową . Reguła opisująca powstanie błędu może wyglądać np. tak:
Pomijamy tutaj reguły dla przypadku, gdy oblicza się do wartości różnej od zera. Ponadto dla czytelności przyjęliśmy, że wynikiem tranzycji jest wyłącznie informacja o błędzie, a stan jest zapominany. Bez trudu możnaby wszystkie reguły (zarówno te powyżej jak i te poniżej) zmodyfikować tak, by wraz z informacją o błędzie zwracany był też stan, w którym błąd się pojawił. Np. ostatnia reguła wyglądałaby następująco:
i zamiast pojedyńczej konfiguracji końcowej potrzebowalibyśmy oczywiście całego zbioru .
Przejdźmy teraz do drugiego punktu. Potrzebujemy dodatkowych reguł, które zagwarantują, że błąd, raz pojawiwszy się, propaguje się przez wszystkie konstrukcje składniowe, a normalne obliczenie wyrażenia jest wstrzymame.
Następnie, błąd w wyrażeniu powinien wstrzymać normalne wykonanie instrukcji:
I wreszcie błąd powinien propagować się do kolejnych instrukcji:
Zadanie 3
Rozszerz język Tiny o następującą instrukcję pętli:
to instrukcja pętli, stanowi instrukcję wewnętrzną. Instrukcja wychodzi z nabliższej pętli i kontynuuje wykonanie programu od pierwszej instrukcji za tą pętlą. Instrukcje powraca na początek instrukcji wewnętrznej najbliższej pętli.
Pozważ zarówno semantykę naturalną jak i semantykę małych kroków.
Rozwiązanie 1 (semantyka naturalna)
Dodamy do reguł semantyki naturalnej dla języka Tiny kilka nowych reguł opisujących nową konstrukcję języka i jej interakcję z pozostałymi konstrukcjami.
Pomysł polega na dodaniu specjalnych konfiguracji zawierających informację o tym, że została wykonana instrukcja lub . Oto odpowiednie reguły:
Czyli instrukcje i nie modyfikują stanu , ale zostawiają po sobie \ślad". Zauważmy, że taki ślad zostaje pozostawiony tylko wtedy, jesli nie było dotychczas innego śladu, to znaczy jeśli (lub ) zostało wykonane w zwykłym stanie . Oczywiście poszerzamy odpowiednio zbiór konfiguracji o:
</math>[ \mathbf{State} \times \{ \mbox{było-}\mathbf{exit}, \mbox{było-}\mathbf{continue} \} </math> , Pytanie: jakie powinno być zachowanie i w konfiguracji lub ? Czy instrukcje i będą faktycznie wykonywane w takich konfiguracjach?
Zapiszmy teraz jak inne instrukcje korzystają z dodatkowej informacji (śladu) zawartej w konfiguracjach. Oczywiście beneficjentem tej informacji jest instrukcji :
Czyli w zależności od tego, jaki ślad został zarejestrowany podczas wykonania , albo kończymy wykonanie pętli , albo rozpoczynamy kolejną iterację. Zauważmy, że stan może być różny od , ponieważ zanim wykonała się ktoraś z instrukcji lub , mogły zostać zmienione wartości niektórych zmiennych.
Oczywiście, jeśli instrukcja wewnętrzna zakończyła się normalnie, kontynuujemy wykonanie pętli podobnie jak w przypadku wywołania :
Pytanie: czy potrzebujemy dodatkowo reguł postaci:
Okazuje się że nie, ponieważ ślad powinien zostać zawsze wymazany przez pętlę . Poza tym reguły te wykraczałyby poza klasyczna podejście semantyki naturalnej, w którym zwykle bezpośrednio definiujemy tranzycje postaci .
Teraz musimy określić zachowanie wszystkich instrukcji w sytuacji, gdy bieżąca konfiguracja zawiera już ślad. Zasadniczo, powinniśmy zaniechać wykonania instrukcji (w przypadku pętli, powinniśmy zaniechać dalszego iterowania tej pętli). Oto odpowiednie reguły dla :
Pominęliśmy zupełnie analogiczne reguły dla konfiguracji . Zwróćmy szczególnie uwagę na ostatnią regułę dla pętli : wyraża ona przypadek, gdy ślad został wygenerowany nie w pierwszym obiegu pętli, ale w którymś z kolejnych. Musieliśmy rozważyc również ten przypadek, ponieważ wybraliśmy podejście dużych kroków; w podejściu małych kroków nie byłoby to zapewne konieczne. Zauważmy też, że dla pętli nie rozpatrujemy przypadku, gdy dozór oblicza się do , gdyż w tym przypadku nie ma możliwości wygenerowania śladu.
Zauważmy, że nasze reguły nie pozwalają na dodanie drugiego (kolejnego) śladu!
Rozwiązanie 2 (małe kroki)
W semantyce naturalnej musieliśmy napisać wiele reguł aby zapewnić pomijanie instrukcji w sytuacji, gdy został juz zarejestrowany jakiś ślad. Było to dość uciążliwe. Okazuje się, że podejście mało-krokowe oferuje możliwość bardziej eleganckiego rozwiązania.
Punktem startowym sę teraz reguły mało-krokowe dla języka Tiny.
Podobnie jak poprzednio rozszerzymy zbiór konfiguracji i podobnie opiszemy, jak powstaje ślad:
Ponadto musimy określić sposób, w jaki mały krok mniejszej instrukcji zostaje zamieniony na mały krok większej. Np.
Zauważmy, że nie musimy zajmowac się przypadkiem, gdy ślad powstaje w , bo wybraliśmy podejście mało-krokowe. Ponadto, nie musimy opisywać instrukcji warunkowej i pętli , ponieważ ślad nie może powstać podczas oblcizania dozoru!
Wreszcie zobaczmy jak zachowuje się pętla :
Reguły te są prawie identyczne do reguł semantyki naturalnej dla tej sytuacji! Natomiast korzystamy z tego, że w podejściu mało-krokowym zmiana konfiguracji na czy jest natychmiast widoczna w instrukcji , nawet jeśli czy zostało wywołane głęboko wewnątrz !
Niestety, powyzsze reguły nie są poprawne! Dlaczego? Jak zwykle w semantyce małych kroków, wykonując instrukcję wewnętrzną zapominamy stopniowo jaka była ona na początku. I w związku z tym nie potrafimy poprawnie powrócić do wykonywania pętli po wywołaniu .
Prostym sposobem poprawienia naszego blędu jest rozszerzenie składni tak, aby możliwe było jednorazowe rozwinięcie pętli :
Teraz możemy zapisać dwie powyższe reguły dla w poprawnej wersji, pamiętając o tym, że i pojawią się nie w instrukcji wewnętrznej, ale w jej kopii umieszczonej przed :
A ponieważ wewnątrz kopii mogą być zagnieżdzone instrukcje potrzebujemy dodatkowej reguły:
Na koniec zauważmy, że stan w pierwszych dwóch z powyższych trzech reguł nigdy nie jest różny od . Zatem równoważnie moglibyśmy zamienić na w powyższych dwóch regułach. Ale wtedy okazuje się , w parze z albo jest nadmiarowe i może zostać wyeliminowane.
Zatem ostatecznie nasze reguły mogą wyglądać tak:
a zbiór konfiguracji poszerzamy tylko o
Zadania domowe
Zadanie 1
Zaproponuj semantykę mało-krokową języka z zdania 2. Czy różni się ona istotnie od semantyki naturalnej?
Zadanie 2
Napisz semantyję naturalną dla nieznacznie rozszerzonej wersji instrukcji :
Identyfikator pełni tutaj rolę etykiety przypisanej instrukcji , jest też parametrem dwóch pozostałych instrukcji. kończy teraz najbliższą otaczającą pętlę o etykiecie . Podobnie wznawia najbliższą pętlę o etykiecie . Np. program
Parser nie mógł rozpoznać (błąd składni): {\displaystyle x: \mathbf{loop}\,\\ \quad \quad a := 1; \quad \quad y: \mathbf{loop}\, \quad \quad \quad \quad \mathbf{exit} x; \quad \quad \quad \quad a := a-10; \quad \quad a := a+1; a := a+2; }
kończy działanie z wartością zmiennej . Zauważmy, że musieliśmy jakoś określić, do wnętrza której pętli należą trzy ostatnie instrukcje. Użyliśmy to tego celu wcięć a 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ę , np. .
Zadanie 3
Napisz semantykę naturalną i mało-krokową dla rozszerzenia języka Tiny o wyrażenia z efektami ubocznymi:
Obliczenie wyrażenia polega na wykonaniu a potem na obliczeniu . Wartość wyrażenia jest taka jak wartość wyrażenia a efektem ubocznym jest podstawienie tej wartości na zmienną .
