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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Mengel (dyskusja | edycje)
Nie podano opisu zmian
 
m Zastępowanie tekstu – „<math> ” na „<math>”
 
(Nie pokazano 42 wersji utworzonych przez 4 użytkowników)
Linia 1: Linia 1:
== Semantyka bezpośrednia instrukcji. Konstrukcje iteracyjne. ==
== Semantyka bezpośrednia instrukcji. Konstrukcje iteracyjne. ==
=== Zadanie 1 ===
=== Pętle '''while''' i '''repeat''' ===
 
{{cwiczenie|1|cw1|


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


<math>
<math>
n \, ::= \,\, 0 \,\,|\,\, 1 \,\,|\,\, \ldots
n \, ::= \ldots \,\, -1\,\,|\,\, 0 \,\,|\,\, 1 \,\,|\,\, \ldots
</math>
</math>


Linia 16: Linia 18:
         n  \,\,|\,\,
         n  \,\,|\,\,
         x  \,\,|\,\,
         x  \,\,|\,\,
         e_1 + e_2  \,\,|\,\,
         e_1\,\, + \,\, e_2
</math>
</math>


<math>
<math>
b \,  ::=  \,\,   
b \,  ::=  \,\,   
         e_1 = e_2  \,\,|\,\,
         e_1\, = \, e_2  \,\,|\,\,
         \mathbf{not}\, b    \,\,|\,\,
         \mathbf{not}\,\, b    \,\,|\,\,
         b_1\, \mathbf{or}\, b_2  \,\,|\,\,
         b_1\,\, \mathbf{or}\,\, b_2
</math>
</math>


<math>
<math>
i \, ::= \,\,
i \, ::= \,\,
         x := e    \,\,|\,\,
         x\, :=\, e    \,\,|\,\,
         i_1; i_2  \,\,|\,\,
         i_1; i_2  \,\,|\,\,
         \mathbf{if}\, b \,\mathbf{then}\, i_1 \,\mathbf{else}\, i_2 \,\,|\,\,
         \mathbf{if}\,\, b \,\,\mathbf{then}\,\, i_1 \,\,\mathbf{else}\,\, i_2 \,\,|\,\,
         \mathbf{skip} \,\,|\,\,
         \mathbf{skip} \,\,|\,\,
         \mathbf{while}\, b \,\mathbf{do}\, i \,\,|\,\,
         \mathbf{while}\,\, b \,\,\mathbf{do}\,\, i \,\,|\,\,
         \mathbf{repeat}\, i \,\mathbf{until}\, b \,\,|\,\,
         \mathbf{repeat}\,\, i \,\mathbf{until}\,\, b
</math>
</math>


Pętla <math> \mathbf{repeat}\, i \,\mathbf{until}\, b </math> 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''.
Pętla <math>\mathbf{repeat}\,\, i \,\,\mathbf{until}\,\, b</math> 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 pinezki we właściwych dziedzinach. Zakładamy, że
wszystkie zmienne są zainicjowane na zero.
 
Użyjemy elementarnych dziedzin z wykładu:
* Int <nowiki>=</nowiki> ..., -1, 0, 1, ... zawierający denotacje stałych
liczbowych
* Bool <nowiki>=</nowiki> {tt}, {ff} zawierający wartości logiczne
* Var zawierający wszystkie dozwolone identyfikatory
 
<div class="mw-collapsible mw-made=collapsible mw-collapsed">
Przypomnijmy, że wartość wyrażenia arytmetycznego <math>e</math> zależy od
<div class="mw-collapsible-content" style="display:none">
wartości wszystkich występujących w nim zmiennych.
</div>
</div>
 
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:
 
<center><math>State = Var \rightarrow Int</math></center>
 
Zdefiniujmy następnie niezbędne funkcje semantyczne.
* Dla wyrażeń mamy
 
<center><math>\mathcal{E} & : & \mathrm Exp \rightarrow \mathrm State \rightarrow \mathrm Int</math></center>
 
* Dla wyrażeń logicznych:
 
<center><math>\mathcal{B} & : & \mathrm BExp \rightarrow \mathrm State \rightarrow \mathrm Bool</math></center>
 
* Dla instrukcji:
 
<center><math>\mathcal{I} & : & \mathrm Stmt \rightarrow \mathrm State \rightarrow \mathrm State</math></center>
 
* Oraz oczywistą funkcję dla stałych całkowitych:
 
<center><math>\mathcal{Z} & : & \mathrm Num \rightarrow \mathcal{Z}</math></center>
 
Funkcji {Z} nie definiujemy, przyjmując jak zwykle, że jej wynikiem
jest wartość stałej liczbowej.
 
Rozpocznijmy od funkcji semantycznej dla wyrażeń. Musimy zdefiniować
znaczenie (wartość) wyrażenia <math>e</math> w pewnym stanie <math>s</math>. Ową wartość
zapisujemy jako <math>\mathcal{E} [\![e]\!] s</math>, czyli wartość funkcji E zastosowanej do
dwóch argumentów: wyrażenia <math>e</math> oraz stanu <math>s</math>. 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:
# Co jest wartością wyrażenia <math>x</math> w stanie <math>s</math>? Odpowiedź: wartość
zmiennej <math>x</math> w tym stanie, czyli wartość uzyskana przez zastosowanie
funkcji <math>s</math> do identyfikatora <math>x</math>. Zapisujemy to następująco:
 
<center><math>\mathcal{E} [\![x]\!] s = s (x)</math></center>
 
Często będziemy pomijać nawiasy przy aplikacji funkcji pisząc po
prostu <math>s\,x</math> zamiast <math>s(x)</math>. To samo można zapisać stosując notację
"lambda":


=== Zadanie 2 ===
<center><math>\mathcal{E} [\![x]\!] = \l s \in \mathrm State.s (x)</math></center>
-->
=== Pętla '''for''' ===
{{cwiczenie|2|cw2|
Rozszerzmy język z poprzedniego zadania o instrukcję:
Rozszerzmy język z poprzedniego zadania o instrukcję:


Linia 51: Linia 130:
# Jeśli <math>x > m</math>, to pętla kończy się.  
# Jeśli <math>x > m</math>, to pętla kończy się.  
# W przeciwnym razie:
# W przeciwnym razie:
#* Wykonujemy instrukcję <math> i </math>.
#* Wykonujemy instrukcję <math>i</math>.
#* Zwiększamy zmienną <math>x</math> o 1.
#* Zwiększamy zmienną <math>x</math> o 1.
#* Powracamy do punktu 3.
#* Powracamy do punktu 3.
Zauważmy, że wyrażenie <math>e_1</math> jest tu wyliczane tylko raz, ale <math>e_2</math> oblicza się przy każdym obrocie pętli.
Zauważmy, że wyrażenie <math>e_1</math> jest tu wyliczane tylko raz, ale <math>e_2</math> oblicza się przy każdym obrocie pętli.
}}
<div class="mw-collapsible mw-made=collapsible mw-collapsed">
<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie</span>
<div class="mw-collapsible-content" style="display:none">
Jeszcze nie ma.
</div>
</div>


=== Zadanie 3 ===
{{cwiczenie|3|cw3|
Zmieńmy semantykę instrukcji for z poprzedniego zadania tak, aby  
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:
oba wyrażenia obliczały się tylko raz. Tym razem wyliczenie pętli polega na:
Linia 67: Linia 156:
#* Zwiększamy zmienną <math>x</math> o 1.
#* Zwiększamy zmienną <math>x</math> o 1.
#* Powracamy do punktu 4.
#* Powracamy do punktu 4.
}}
<div class="mw-collapsible mw-made=collapsible mw-collapsed">
<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie</span>
<div class="mw-collapsible-content" style="display:none">
Jeszcze nie ma.
</div>
</div>
{{cwiczenie| 4|cw4|
O pętli '''for''' można jednak myśleć jeszcze inaczej. Można wymagać, aby wszelkie zmiany wartości zmiennej sterującej <math>x</math> 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 :<nowiki>=</nowiki> 1 '''to''' 10 '''do'''
  x:<nowiki>=</nowiki> x + 1;
  y:<nowiki>=</nowiki> y + x;
wykonuje się pięć razy, a zmienna <math>y</math> jest zwiększana łącznie o 2+4+6+8+10. Jeśli uznamy, że zmiany zmiennej <math>x</math> wewnątrz pętli nie wpływają na liczbę iteracji, to pętla wykona się 10 razy, a zmienna <math>y</math> zostanie zwiększona o 2+3+4+5+6+7+8+9+10+11.
Zdefiniuj taką semantykę.
}}
<div class="mw-collapsible mw-made=collapsible mw-collapsed">
<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie</span>
<div class="mw-collapsible-content" style="display:none">
Jeszcze nie ma.
</div>
</div>


=== Zadanie 4 ===
O pętli for można jednak myśleć jeszcze inaczej. Można wymagać, aby wszelkie zmiany wartości zmiennej sterującej <math>x</math> 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. Zdefiniuj taką semantykę.


=== Zadanie 5 ===
{{cwiczenie|5|cw5|
W języku C pętla '''for''' ma następującą postać:
W języku C pętla '''for''' ma następującą postać:
<math>
<math>
Linia 86: Linia 196:
# Jeśli wyrażenie wylicza się do fałszu, to pętla kończy się.  
# Jeśli wyrażenie wylicza się do fałszu, to pętla kończy się.  
# W przeciwnym razie:
# W przeciwnym razie:
#* Wykonujemy instrukcję <math> i_3 </math>.
#* Wykonujemy instrukcję <math>i_3</math>.
#* Wykonujemy instrukcję <math> i_2 </math>.
#* Wykonujemy instrukcję <math>i_2</math>.
#* Powracamy do punktu 2.
#* Powracamy do punktu 2.
}}
<div class="mw-collapsible mw-made=collapsible mw-collapsed">
<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie</span>
<div class="mw-collapsible-content" style="display:none">
Jeszcze nie ma.
</div>
</div>

Aktualna wersja na dzień 22:13, 11 wrz 2023

Semantyka bezpośrednia instrukcji. Konstrukcje iteracyjne.

Pętle while i repeat

Ćwiczenie 1

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

n::=1|0|1|

x::=(identyfikatory)

e::=n|x|e1+e2

b::=e1=e2|𝐧𝐨𝐭b|b1𝐨𝐫b2

i::=x:=e|i1;i2|𝐢𝐟b𝐭𝐡𝐞𝐧i1𝐞𝐥𝐬𝐞i2|𝐬𝐤𝐢𝐩|𝐰𝐡𝐢𝐥𝐞b𝐝𝐨i|𝐫𝐞𝐩𝐞𝐚𝐭i𝐮𝐧𝐭𝐢𝐥b

Pętla 𝐫𝐞𝐩𝐞𝐚𝐭i𝐮𝐧𝐭𝐢𝐥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.

Pętla for

Ćwiczenie 2

Rozszerzmy język z poprzedniego zadania o instrukcję:

i::=𝐟𝐨𝐫x:=e1𝐭𝐨e2𝐝𝐨i

Wykonanie takiej pętli polega na:

  1. Wyliczeniu wartości n wyrażenia e1.
  2. Przypisaniu wartości n na zmienną x.
  3. Wyliczeniu wartości m wyrażenia e2.
  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 e1 jest tu wyliczane tylko raz, ale e2 oblicza się przy każdym obrocie pętli.


Rozwiązanie


Ć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 e1.
  2. Przypisaniu wartości n na zmienną x.
  3. Wyliczeniu wartości m wyrażenia e2.
  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


Ćwiczenie 4

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. Zdefiniuj taką semantykę.


Rozwiązanie


Ćwiczenie 5

W języku C pętla for ma następującą postać: i::=𝐟𝐨𝐫(i1;b;i2)i3

Jej wykonanie polega na:

  1. Wykonaniu instrukcji i1.
  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ę i3.
    • Wykonujemy instrukcję i2.
    • Powracamy do punktu 2.


Rozwiązanie