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

← poprzednia edycja następna edycja →

WizualnieWikikod

Wersja z 15:01, 29 wrz 2006

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 44: / Linia 44: @@
 Deklaracja <math>\mathbf{fun}\, F (x); i\, \mathbf{endfun}
-</math> wprowadza funkcję o nazwie ''F'' z jednym parametrem ''x'' przekazywanym
+</math> wprowadza funkcję o nazwie <math>F</math> z jednym parametrem <math>x</math> przekazywanym
-przez zmienną. Wykonanie funkcji polega na wykonaniu instrukcji ''i'', która
+przez zmienną. Wykonanie funkcji polega na wykonaniu instrukcji <math>i</math>, która
-powinna zawierać przypisanie na identyfikator ''F''. Takie przypisanie ustala
+powinna zawierać przypisanie na identyfikator <math>F</math>. 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:
+Powróćmy do języka TINY. Dodajmy do niego następujące instrukcje:
 <math>
@@ Linia 133: / Linia 133: @@
      '''end'''
    '''end'''
-zakończy się ze zmienną x równą 2.
+zakończy się ze zmienną <math>x</math> równą 2.
-Choć środowiska wydają się tu niepotrzebne spróbuj wykorzystać je do
+Choć środowiska wydają się tu niepotrzebne, spróbuj wykorzystać je do
 przechowywania pewnych potrzebnych informacji.

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

Wersja z 15:01, 29 wrz 2006

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