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ę {\bf 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 = \{\ldots, -1, 0, 1, \ldots\} 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 \ra Int \]

Zdefiniujmy następnie niezbędne funkcje semantyczne.

• Dla wyrażeń mamy

\[\E & : & Exp \ra State \ra Int \]

• Dla wyrażeń logicznych:

\[\B & : & BExp \ra State \ra Bool \]

• Dla instrukcji:

\[\I & : & Stmt \ra Stmt \ra Stmt \]

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

\[\Z & : & Num \ra Z \]

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}}}