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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
← poprzednia edycja
WizualnieWikikod
m Zastępowanie tekstu – „<math> ” na „<math>”
 
(Nie pokazano 2 pośrednich wersji utworzonych przez tego samego użytkownika)
Linia 38: Linia 38:
</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''.
}}
}}
<!--
<!--
Linia 73: Linia 73:
Var w zbiór Int. Zbiór wszystkich stanów to:
Var w zbiór Int. Zbiór wszystkich stanów to:


<center><math>State = Var \rightarrow Int </math></center>
<center><math>State = Var \rightarrow Int</math></center>


Zdefiniujmy następnie niezbędne funkcje semantyczne.  
Zdefiniujmy następnie niezbędne funkcje semantyczne.  
* Dla wyrażeń mamy  
* Dla wyrażeń mamy  


<center><math>\mathcal{E} & : & \mathrm Exp \rightarrow \mathrm State \rightarrow \mathrm Int </math></center>
<center><math>\mathcal{E} & : & \mathrm Exp \rightarrow \mathrm State \rightarrow \mathrm Int</math></center>


* Dla wyrażeń logicznych:  
* Dla wyrażeń logicznych:  


<center><math>\mathcal{B} & : & \mathrm BExp \rightarrow \mathrm State \rightarrow \mathrm Bool </math></center>
<center><math>\mathcal{B} & : & \mathrm BExp \rightarrow \mathrm State \rightarrow \mathrm Bool</math></center>


* Dla instrukcji:
* Dla instrukcji:


<center><math>\mathcal{I} & : & \mathrm Stmt \rightarrow \mathrm State \rightarrow \mathrm State </math></center>
<center><math>\mathcal{I} & : & \mathrm Stmt \rightarrow \mathrm State \rightarrow \mathrm State</math></center>


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


<center><math>\mathcal{Z} & : & \mathrm Num \rightarrow \mathcal{Z} </math></center>
<center><math>\mathcal{Z} & : & \mathrm Num \rightarrow \mathcal{Z}</math></center>


Funkcji {Z} nie definiujemy, przyjmując jak zwykle, że jej wynikiem
Funkcji {Z} nie definiujemy, przyjmując jak zwykle, że jej wynikiem
Linia 130: 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.
Linia 196: 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.
}}
}}

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

Źródło: „https://wazniak.mimuw.edu.pl/index.php?title=Semantyka_i_weryfikacja_programów/Ćwiczenia_7&oldid=82504”