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

← poprzednia edycja

WizualnieWikikod

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

Funkcje

Zadanie 1

Zdefiniuj semantykę denotacyjną 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} | 𝐜 𝐚 𝐥 𝐥 F (x)$

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

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

$d : : = 𝐯 𝐚 𝐫 x : = e | d_{1}; d_{2} | 𝐟 𝐮 𝐧 F (x); i 𝐞 𝐧 𝐝 𝐟 𝐮 𝐧$

Deklaracja $𝐟 𝐮 𝐧 F (x); i 𝐞 𝐧 𝐝 𝐟 𝐮 𝐧$ wprowadza funkcję o nazwie $F$ z jednym parametrem $x$ przekazywanym przez zmienną. Wykonanie funkcji polega na wykonaniu instrukcji $i$ , która powinna zawierać przypisanie na identyfikator $F$ . Takie przypisanie ustala wartość funkcji ale nie kończy wykonania instrukcji i.

Kontynuacje instrukcji

Zadanie 2

Powróćmy do języka TINY. Dodajmy do niego następujące instrukcje:

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

Zdefiniuj semantykę kontynuacyjną powyższych instrukcji. Możesz przy tym korzystać z gotowych już funkcji semantycznych dla pozostałych kategorii (w semantyce bezpośredniej) syntaktycznych.

Zadanie 3

Rozszerz język z poprzedniego zadania o konstrukcje

$i : : = 𝐥 𝐨 𝐨 𝐩 i 𝐞 𝐧 𝐝 𝐥 𝐨 𝐨 𝐩 | 𝐛 𝐫 𝐞 𝐚 𝐤 | 𝐜 𝐨 𝐧 𝐭 𝐢 𝐧 𝐮 𝐞$

Zadanie 4

Uzupełnij definicję języka o bloki, deklaracje zmiennych i procedur oraz wywołanie procedury.

Zadanie 5

Zdefiniuj semantykę denotacyjną 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} | 𝐜 𝐚 𝐥 𝐥 F (x)$

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

$p : : = 𝐛 𝐞 𝐠 𝐢 𝐧 i 𝐞 𝐧 𝐝$

Program i instukcje postaci $𝐛 𝐞 𝐠 𝐢 𝐧 i 𝐞 𝐧 𝐝$ są blokami. Instrukcja break powoduje natychmiastowe wyjście z bloku i wznowienie wykonania od następnej instrukcji po bloku. Instrukcja again to skok do pierwszej instrukcji w najbardziej zagnieżdżonym bloku, w którym wystąpiła. Instrukcja rollback działa podobnie jak break, ale anuluje wszystkie zmiany dokonane od ostatniego wejścia do bloku, w którym wystąpiła.

Wykonanie programu:

 begin
   x := 2;
   begin
     x := x + 1;
     if x = 5 then rollback else again
   end
 end

zakończy się ze zmienną $x$ równą 2. Choć środowiska wydają się tu niepotrzebne, spróbuj wykorzystać je do przechowywania pewnych potrzebnych informacji.

@@ Linia 118: / Linia 118: @@
 </math>
-Program i instukcje postaci <math> \mathbf{begin}\, i \, \mathbf{end}</math> są blokami.
+Program i instukcje postaci <math>\mathbf{begin}\, i \, \mathbf{end}</math> są blokami.
 Instrukcja '''break''' powoduje natychmiastowe wyjście z bloku i wznowienie
 wykonania od następnej instrukcji po bloku. Instrukcja '''again''' to skok do

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

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

Spis treści

Funkcje

Zadanie 1

Kontynuacje instrukcji

Zadanie 2

Zadanie 3

Zadanie 4

Zadanie 5

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia