Semantyka i weryfikacja programów/Ćwiczenia 7

Semantyka bezpośrednia instrukcji. Konstrukcje iteracyjne.

Pętle while i repeat

Ćwiczenie 1

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

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

$x::=\dots (identyfikatory)\dots$

$e::=n|x|e_1+e_2$

$b::=e_1=e_2|\mathbf{𝐧}\mathbf{𝐨}\mathbf{𝐭}b|b_1\mathbf{𝐨}\mathbf{𝐫}{b}_2$

$i::=x:=e|i_1;i_2|\mathbf{𝐢}\mathbf{𝐟}b\mathbf{𝐭}\mathbf{𝐡}\mathbf{𝐞}\mathbf{𝐧}{i}_1\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{i}_2|\mathbf{𝐬}\mathbf{𝐤}\mathbf{𝐢}\mathbf{𝐩}|\mathbf{𝐰}\mathbf{𝐡}\mathbf{𝐢}\mathbf{𝐥}\mathbf{𝐞}b\mathbf{𝐝}\mathbf{𝐨}i|\mathbf{𝐫}\mathbf{𝐞}\mathbf{𝐩}\mathbf{𝐞}\mathbf{𝐚}\mathbf{𝐭}i\mathbf{𝐮}\mathbf{𝐧}\mathbf{𝐭}\mathbf{𝐢}\mathbf{𝐥}b$

Pętla $\mathbf{𝐫}\mathbf{𝐞}\mathbf{𝐩}\mathbf{𝐞}\mathbf{𝐚}\mathbf{𝐭}i\mathbf{𝐮}\mathbf{𝐧}\mathbf{𝐭}\mathbf{𝐢}\mathbf{𝐥}b$ polega na wykonaniu instrukcji i, a następnie wyliczeniu warunku logicznego b. Jeśli warunek jest prawdziwy wykonanie pętli kończy się, w przeciwnym razie powracamy do wykonania instrukcji i.

Powyższy język to tak naprawdę Tiny z wykładu rozszerzony o jedną konstrukcję: pętlę repeat. Spróbuj wykonać to ćwiczenie nie sięgając do notatek z wykładu. Jeśli napotkasz trudności, odkrywaj kolejne elementy poniższego opisu.

Kategorie składniowe występujące w tym języku to:

• wyrażenia Exp
• wyrażenia logiczne BExp
• instrukcje Stmt
• oraz, jak zwykle, stałe liczbowe Num

Zaczynamy jak zwykle od opisu dziedzin semantycznych. Nie przejmujemy się na razie szczegółami związanymi z konstrukcjami stałopunktowymi oraz umieszczeniem pineski we właściwych dziedzinach. Zakładamy, że wszystkie zmienne są zainicjowane na zero.

Użyjemy elementarnych dziedzin z wykładu:

• Int = ..., -1, 0, 1, ... zawierający denotacje stałych

liczbowych

• Bool = {tt}, {ff} zawierający wartości logiczne
• Var zawierający wszystkie dozwolone identyfikatory

Przypomnijmy, że wartość wyrażenia arytmetycznego $e$ zależy od

wartości wszystkich występujących w nim zmiennych.

Wartości te są "pamiętane" w stanie, który jest funkcją ze zbioru Var w zbiór Int. Zbiór wszystkich stanów to:

$State=Var\to Int$

Zdefiniujmy następnie niezbędne funkcje semantyczne.

• Dla wyrażeń mamy

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathcal{E} & : & \mathrm Exp \rightarrow \mathrm State \rightarrow \mathrm Int }

• Dla wyrażeń logicznych:

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathcal{B} & : & \mathrm BExp \rightarrow \mathrm State \rightarrow \mathrm Bool }

• Dla instrukcji:

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathcal{I} & : & \mathrm Stmt \rightarrow \mathrm State \rightarrow \mathrm State }

• Oraz oczywistą funkcję dla stałych całkowitych:

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathcal{Z} & : & \mathrm Num \rightarrow \mathcal{Z} }

Funkcji {Z} nie definiujemy, przyjmując jak zwykle, że jej wynikiem jest wartość stałej liczbowej.

Rozpocznijmy od funkcji semantycznej dla wyrażeń. Musimy zdefioniować znaczenie (wartość) wyrażenia $e$ w pewnym stanie $s$. Ową wartość zapisujemy jako ${ℰ}[[e]]s$, czyli wartość funkcji E zastosowanej do dwóch argumentów: wyrażenia $e$ oraz stanu $s$. Przypomnijmy, że taka "dziwna" notacja z nawiasami służy oddzieleniu składni od elementów z metajęzyka.

Funkcje semantyczne definiujemy dla każdej postaci wyrażenia, odpowiadając na standardowe pytania:

1. Co jest wartością wyrażenia $x$ w stanie $s$, Odpowiedź: wartość

zmiennej $x$ w tym stanie, czyli wartość uzyskana przez zastosowanie funkcji $s$ do identyfikatora $x$. Zapisujemy to następująco

${ℰ}[[x]]s=s(x)$

Często będziemy powijać nawiasy przy aplikacji funkcji pisząc po prostu $sx$ zamiast $s(x)$. To samo można zapisać stosując notację "lambda":

Parser nie mógł rozpoznać (nieznana funkcja „\l”): {\displaystyle \mathcal{E} [\![x]\!] = \l s \in \mathrm State.s (x)}

Pętla for

Ćwiczenie 2

Rozszerzmy język z poprzedniego zadania o instrukcję:

$i::=\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}x:=e_1\mathbf{𝐭}\mathbf{𝐨}{e}_2\mathbf{𝐝}\mathbf{𝐨}i$

Wykonanie takiej pętli polega na:

1. Wyliczeniu wartości $n$ wyrażenia $e_1$.
2. Przypisaniu wartości $n$ na zmienną $x$.
3. Wyliczeniu wartości $m$ wyrażenia $e_2$.
4. Jeśli $x>m$, to pętla kończy się.
5. W przeciwnym razie:
   • Wykonujemy instrukcję $i$.
   • Zwiększamy zmienną $x$ o 1.
   • Powracamy do punktu 3.

Zauważmy, że wyrażenie $e_1$ jest tu wyliczane tylko raz, ale $e_2$ oblicza się przy każdym obrocie pętli.

Rozwiązanie

{{{3}}}

Ćwiczenie 3

Zmieńmy semantykę instrukcji for z poprzedniego zadania tak, aby oba wyrażenia obliczały się tylko raz. Tym razem wyliczenie pętli polega na:

1. Wyliczeniu wartości $n$ wyrażenia $e_1$.
2. Przypisaniu wartości $n$ na zmienną $x$.
3. Wyliczeniu wartości $m$ wyrażenia $e_2$.
4. Jeśli $x>m$, to pętla kończy się.
5. W przeciwnym razie:
   • Wykonujemy instrukcję $i$.
   • Zwiększamy zmienną $x$ o 1.
   • Powracamy do punktu 4.

Rozwiązanie

{{{3}}}

O pętli for można jednak myśleć jeszcze inaczej. Można wymagać, aby wszelkie zmiany wartości zmiennej sterującej $x$ wewnątrz wykonania pętli nie miały wpływu na liczbę iteracji tej pętli. Przykładowo przy semantyce z poprzedniego zadania pętla:

for x := 1 to 10 do 
  x := x + 1;
  y := y + x;

wykonuje}} się pięć razy, a zmienna y jest zwiększana łącznie o 2+4+6+8+10. Jeśli uznamy, że zmiany zmiennej x wewnątrz pętli nie wpływają na liczbę iteracji, to pętla wykona się 10 razy, a zmienna y zostanie zwiększona o 2+3+4+5+6+7+8+9+10+11.

Ćwiczenie 4

Zdefiniuj taką semantykę.

Rozwiązanie

{{{3}}}

Ćwiczenie 5

W języku C pętla for ma następującą postać: $i::=\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}(i_1;b;i_2)i_3$

Jej wykonanie polega na:

1. Wykonaniu instrukcji $i_1$.
2. Wyliczeniu wartości wyrażenia $b$.
3. Jeśli wyrażenie wylicza się do fałszu, to pętla kończy się.
4. W przeciwnym razie:
   • Wykonujemy instrukcję $i_3$.
   • Wykonujemy instrukcję $i_2$.
   • Powracamy do punktu 2.

Rozwiązanie

{{{3}}}