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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
 
Linia 21: Linia 21:
  
  
{{rozwiazanie||roz1|
 
  
<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
+
 
 +
<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">
  
 
Najpierw musimy odgadnąć asercję, którą można wpisać pomiędzy początkowe przypisania a pętlę:
 
Najpierw musimy odgadnąć asercję, którą można wpisać pomiędzy początkowe przypisania a pętlę:
Linia 257: Linia 259:
  
 
</div></div>
 
</div></div>
}}
 
  
  
Linia 276: Linia 277:
  
  
{{rozwiazanie||roz2|
 
  
<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
+
 
 +
<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">
  
 
<math>
 
<math>
Linia 295: Linia 298:
  
 
</div></div>
 
</div></div>
}}
+
 
  
  
Linia 316: Linia 319:
 
Wyrażenie odd(q) ma wartość <math>\mathbf{true}</math> wtedy i tylko wtedy, gdy q jest nieparzyste.
 
Wyrażenie odd(q) ma wartość <math>\mathbf{true}</math> wtedy i tylko wtedy, gdy q jest nieparzyste.
  
{{rozwiazanie||roz3|
 
  
<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
+
 
 +
<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">
  
 
Jako niezmiennik pętli przyjmijmy <math>N \, \equiv \, z {\cdot} p^q = x^y</math>. Oto odpowiednie anotacje naszego programu:
 
Jako niezmiennik pętli przyjmijmy <math>N \, \equiv \, z {\cdot} p^q = x^y</math>. Oto odpowiednie anotacje naszego programu:
Linia 411: Linia 416:
  
 
</div></div>
 
</div></div>
}}
 
  
  
Linia 420: Linia 424:
  
  
{{rozwiazanie||roz4|
 
  
<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
+
<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">
  
 
<math>\mathbf{repeat}\, I \,\mathbf{until}\, b</math> zachowuje się tak samo jak <math>I; \mathbf{while}\, \neg b \,\mathbf{do}\, I</math>.
 
<math>\mathbf{repeat}\, I \,\mathbf{until}\, b</math> zachowuje się tak samo jak <math>I; \mathbf{while}\, \neg b \,\mathbf{do}\, I</math>.
Linia 465: Linia 470:
  
 
</div></div>
 
</div></div>
}}
 
 
  
 
== Zadania domowe ==
 
== Zadania domowe ==

Aktualna wersja na dzień 13:31, 1 cze 2020

Zawartość

Poprawność częściowa prostych programów w języku TINY.


Poprawność częściowa

Ćwiczenie 1

Przeprowadź dowód poprawności częściowej poniższego programu:



x := 1; y := 0;
while x <= n do
  y := y + x;
  x := x + 1



Rozwiązanie


Ćwiczenie 2

Uzupełnij poniższe reguły:



Rozwiązanie


Ćwiczenie 3 (potęgowanie binarne)

Dowiedź poprawności częściowej poniższego programu:



z := 1; p := x; q := y;
while q <> 0 do
  if odd(q) then
    z := z * p;
  q := q div 2;
  p := p * p


Wyrażenie odd(q) ma wartość wtedy i tylko wtedy, gdy q jest nieparzyste.


Rozwiązanie


Ćwiczenie 4

Zaproponuj regułę dla instrukcji .


Rozwiązanie

Zadania domowe

Ćwiczenie 1

Wyprowadź ostatnią regułę dla pętli z pierwszej reguły.


Ćwiczenie 2

Napisz program obliczający największy wspólny dzielnik dwóch liczb i przeprowadź dowód poprawności częściowej.


Ćwiczenie 3

Przeprowadź dowód poprawności częściowej:



a = 1; b := 1; y := 1;
while y <= x do
  y := y + 3*a + 3*b + 1;
  a = a + 2*b + 1;
  b := b + 1;


Wskazówka