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::=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.

Rozwiązanie

{{{3}}}

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