Semantyka i weryfikacja programów/Ćwiczenia 12: Różnice pomiędzy wersjami
m Zastępowanie tekstu – „<math> ” na „<math>” |
|||
| Linia 38: | Linia 38: | ||
</math> | </math> | ||
Znaczenie wszystkich konstrukcji z wyjątkiem <math> \mathbf{for}\, x = e_1\, \mathbf{to}\, e_2 \, \mathbf{try}\, i_1\, \mathbf{else}\, i_2</math> oraz <math>\mathbf{fail}</math> jest standardowe. | Znaczenie wszystkich konstrukcji z wyjątkiem <math>\mathbf{for}\, x = e_1\, \mathbf{to}\, e_2 \, \mathbf{try}\, i_1\, \mathbf{else}\, i_2</math> oraz <math>\mathbf{fail}</math> jest standardowe. | ||
Znaczenie instrukcji <math> \mathbf{for}\, x = e_1\, \mathbf{to}\, e_2\, \mathbf{try}\, i_1\, \mathbf{else}\, i_2</math> jest następujące: najpierw jeden raz jest obliczana wartość wyrażenia <math>e_1</math> i podstawiana na zmienną <math>x</math>. Potem w pętli robimy co następuje: jeśli <math>x > e_2</math>, to | Znaczenie instrukcji <math>\mathbf{for}\, x = e_1\, \mathbf{to}\, e_2\, \mathbf{try}\, i_1\, \mathbf{else}\, i_2</math> jest następujące: najpierw jeden raz jest obliczana wartość wyrażenia <math>e_1</math> i podstawiana na zmienną <math>x</math>. Potem w pętli robimy co następuje: jeśli <math>x > e_2</math>, to | ||
wykonujemy <math>i_2</math> w stanie sprzed instrukcji '''for''' (w szczególności wartość zmiennej <math>x</math> na początku wykonywania <math>i_2</math> powinna być przywrócona do tej sprzed wykonania instrukcji '''for''') i przechodzimy do dalszej części programu. Natomiast jeśli <math>x \leq e_2</math>, to jest wykonywana instrukcja <math>i_1</math>. Jeśli w <math>i_1</math> nie zostanie napotkana instrukcja '''fail''', to przywracamy starą wartość zmiennej <math>x</math> (tę sprzed wykonania instrukcji '''for''') i przechodzimy do dalszej części programu. Jeśli jednak napotkamy '''fail''', to przywracamy stan sprzed wykonania instrukcji '''for''' (zachowując oczywiście wartość zmiennej <math>x</math>), zwiększamy wartość zmiennej <math>x</math> o 1 i powtarzamy procedurę opisaną powyżej. | wykonujemy <math>i_2</math> w stanie sprzed instrukcji '''for''' (w szczególności wartość zmiennej <math>x</math> na początku wykonywania <math>i_2</math> powinna być przywrócona do tej sprzed wykonania instrukcji '''for''') i przechodzimy do dalszej części programu. Natomiast jeśli <math>x \leq e_2</math>, to jest wykonywana instrukcja <math>i_1</math>. Jeśli w <math>i_1</math> nie zostanie napotkana instrukcja '''fail''', to przywracamy starą wartość zmiennej <math>x</math> (tę sprzed wykonania instrukcji '''for''') i przechodzimy do dalszej części programu. Jeśli jednak napotkamy '''fail''', to przywracamy stan sprzed wykonania instrukcji '''for''' (zachowując oczywiście wartość zmiennej <math>x</math>), zwiększamy wartość zmiennej <math>x</math> o 1 i powtarzamy procedurę opisaną powyżej. | ||
Aktualna wersja na dzień 22:12, 11 wrz 2023
Semantyka kontynuacyjna
Zadanie 1
Zdefiniuj kontynuacyjną semantykę następującego języka:
Znaczenie wszystkich konstrukcji z wyjątkiem oraz jest standardowe.
Znaczenie instrukcji jest następujące: najpierw jeden raz jest obliczana wartość wyrażenia i podstawiana na zmienną . Potem w pętli robimy co następuje: jeśli , to wykonujemy w stanie sprzed instrukcji for (w szczególności wartość zmiennej na początku wykonywania powinna być przywrócona do tej sprzed wykonania instrukcji for) i przechodzimy do dalszej części programu. Natomiast jeśli , to jest wykonywana instrukcja . Jeśli w nie zostanie napotkana instrukcja fail, to przywracamy starą wartość zmiennej (tę sprzed wykonania instrukcji for) i przechodzimy do dalszej części programu. Jeśli jednak napotkamy fail, to przywracamy stan sprzed wykonania instrukcji for (zachowując oczywiście wartość zmiennej ), zwiększamy wartość zmiennej o 1 i powtarzamy procedurę opisaną powyżej.
Instrukcja fail poza instrukcją for powinna powodować natychmiastowe zakończenie wykonywania programu. Jeśli fail występuję po else, czyli w , to odnosi się ono do (być może nieistniejącej) zewnętrznej pętli for.
Zadanie 2
Oto pewien śmieszny język programowania:
Programy w tym języku mogą wykonywać się w dwie strony: od lewej do prawej oraz od prawej do lewej. Wykonanie rozpoczyna się od pierwszej instrukcji i przebiega od lewej do prawej. Instrukcja back powoduje zmianę kierunku wykonania. Instrukcja left i powoduje wykonanie i jeśli wykonanie przebiega od prawej do lewej, w przeciwnym razie jest to instrukcja pusta. Symetrycznie działa right. Napisz semantykę tego języka.
