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

← poprzednia edycja

WizualnieWikikod

Aktualna wersja na dzień 22:12, 11 wrz 2023

Semantyka kontynuacyjna

Zadanie 1

Zdefiniuj kontynuacyjną semantykę następującego języka:

$n : : = 0 | 1 | \dots$

$x : : = \dots (i d e n t y f i k a t o r y) \dots$

$e : : = n | x | e_{1} + e_{2}$

$b : : = e_{1} < = e_{2} | 𝐧 𝐨 𝐭 b | b_{1} 𝐨 𝐫 b_{2} | 𝐭 𝐫 𝐮 𝐞$

$i : : = x : = e | i_{1}; i_{2} | 𝐢 𝐟 b 𝐭 𝐡 𝐞 𝐧 i_{1} 𝐞 𝐥 𝐬 𝐞 i_{2} | 𝐬 𝐤 𝐢 𝐩 | 𝐟 𝐨 𝐫 x = e_{1} 𝐭 𝐨 e_{2} 𝐭 𝐫 𝐲 i_{1} 𝐞 𝐥 𝐬 𝐞 i_{2} | 𝐟 𝐚 𝐢 𝐥 | 𝐛 𝐞 𝐠 𝐢 𝐧 d; i 𝐞 𝐧 𝐝$

Znaczenie wszystkich konstrukcji z wyjątkiem $𝐟 𝐨 𝐫 x = e_{1} 𝐭 𝐨 e_{2} 𝐭 𝐫 𝐲 i_{1} 𝐞 𝐥 𝐬 𝐞 i_{2}$ oraz $𝐟 𝐚 𝐢 𝐥$ jest standardowe.

Znaczenie instrukcji $𝐟 𝐨 𝐫 x = e_{1} 𝐭 𝐨 e_{2} 𝐭 𝐫 𝐲 i_{1} 𝐞 𝐥 𝐬 𝐞 i_{2}$ jest następujące: najpierw jeden raz jest obliczana wartość wyrażenia $e_{1}$ i podstawiana na zmienną $x$ . Potem w pętli robimy co następuje: jeśli $x > e_{2}$ , to wykonujemy $i_{2}$ w stanie sprzed instrukcji for (w szczególności wartość zmiennej $x$ na początku wykonywania $i_{2}$ powinna być przywrócona do tej sprzed wykonania instrukcji for) i przechodzimy do dalszej części programu. Natomiast jeśli $x \leq e_{2}$ , to jest wykonywana instrukcja $i_{1}$ . Jeśli w $i_{1}$ nie zostanie napotkana instrukcja fail, to przywracamy starą wartość zmiennej $x$ (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 $x$ ), zwiększamy wartość zmiennej $x$ 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 $i_{2}$ , to odnosi się ono do (być może nieistniejącej) zewnętrznej pętli for.

Zadanie 2

Oto pewien śmieszny język programowania:

$i : : = x : = e | i_{1}; i_{2} | 𝐢 𝐟 e 𝐭 𝐡 𝐞 𝐧 i_{1} 𝐞 𝐥 𝐬 𝐞 i_{2} | 𝐬 𝐤 𝐢 𝐩 | 𝐛 𝐚 𝐜 𝐤 | 𝐥 𝐞 𝐟 𝐭 i | 𝐫 𝐢 𝐠 𝐡 𝐭 i$

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.

@@ Linia 38: / Linia 38: @@
 </math>
-Znaczenie wszystkich konstrukcji z wyjątkiem <math> \mathbf{for}\, x = e_1\, \mathbf{to}\, e_2 \, \mathb{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.
 Instrukcja '''fail''' poza instrukcją '''for''' powinna powodować natychmiastowe zakończenie wykonywania programu. Jeśli '''fail''' występuję po '''else''', czyli w <math>i_2</math>, to odnosi się ono do (być może nieistniejącej) zewnętrznej pętli '''for'''.
 === Zadanie 2 ===

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

Aktualna wersja na dzień 22:12, 11 wrz 2023

Semantyka kontynuacyjna

Zadanie 1

Zadanie 2

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia