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\,::=\ldots \,\,-1\,\,|\,\,0\,\,|\,\,1\,\,|\,\,\ldots$

$x\,::=\,\,\ldots \,(identyfikatory)\,\ldots$

$e\,::=\,\,n\,\,|\,\,x\,\,|\,\,e_{1}\,\,+\,\,e_{2}$

$b\,::=\,\,e_{1}\,=\,e_{2}\,\,|\,\,\mathbf {not} \,\,b\,\,|\,\,b_{1}\,\,\mathbf {or} \,\,b_{2}$

$i\,::=\,\,x\,:=\,e\,\,|\,\,i_{1};i_{2}\,\,|\,\,\mathbf {if} \,\,b\,\,\mathbf {then} \,\,i_{1}\,\,\mathbf {else} \,\,i_{2}\,\,|\,\,\mathbf {skip} \,\,|\,\,\mathbf {while} \,\,b\,\,\mathbf {do} \,\,i\,\,|\,\,\mathbf {repeat} \,\,i\,\mathbf {until} \,\,b$

Pętla $\mathbf {repeat} \,\,i\,\,\mathbf {until} \,\,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\rightarrow 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 ${\mathcal {E}}[\![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

${\mathcal {E}}[\![x]\!]s=s(x)$

Często będziemy powijać nawiasy przy aplikacji funkcji pisząc po prostu $s\,x$ 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 {for} \,x\,:=\,e_{1}\,\mathbf {to} \,e_{2}\,\mathbf {do} \,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}}}

Ćwiczenie 4

{{{3}}}

Rozwiązanie

{{{3}}}

Ćwiczenie 5

W języku C pętla for ma następującą postać: $i\,::=\mathbf {for} \,(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}}}