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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
← poprzednia edycjanastępna edycja →
WizualnieWikikod
Sl (dyskusja | edycje)
101 edycji
Nie podano opisu zmian
Sl (dyskusja | edycje)
101 edycji
Nie podano opisu zmian
Linia 121: Linia 121:


  <math>{\color{Red}\{N \land x \leq n\}}</math>
  <math>{\color{Red}\{N \land x \leq n\}}</math>
      <math>{\color{Green}\Downarrow}</math>          <span style="color:brown">// tę implikację należy udowodnić </span>
    <math>{\color{Green}\Downarrow}</math>          <span style="color:brown">// tę implikację należy udowodnić </span>
  <math>{\color{Red}\{N[x \mapsto x{+}1]\}}</math>
  <math>{\color{Red}\{N[x \mapsto x{+}1]\}}</math>
  y := y + x;
  y := y + x;
Linia 139: Linia 139:
  y := 0;
  y := 0;
  <math>{\color{Red}\{n \geq 0 \land x = 1 \land y = 0\}}</math>
  <math>{\color{Red}\{n \geq 0 \land x = 1 \land y = 0\}}</math>
      <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 1 </span>
    <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 1 </span>
  <math>{\color{Red}\{N\}}</math>
  <math>{\color{Red}\{N\}}</math>
  while x <= n do
  while x <= n do
  (
  (
   <math>{\color{Red}\{N \land x \leq n\}}</math>
   <math>{\color{Red}\{N \land x \leq n\}}</math>
        <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 2 </span>
      <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 2 </span>
   <math>{\color{Red}\{N[x \mapsto x{+}1][y \mapsto y{+}x]\}}</math>
   <math>{\color{Red}\{N[x \mapsto x{+}1][y \mapsto y{+}x]\}}</math>
   y := y + x;
   y := y + x;
Linia 152: Linia 152:
  )
  )
  <math>{\color{Red}\{N \land x > n\}}</math>
  <math>{\color{Red}\{N \land x > n\}}</math>
      <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 3 </span>
    <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 3 </span>
  <math>{\color{Red}\{y=\frac{n\cdot(n+1)}{2}\}}</math>
  <math>{\color{Red}\{y=\frac{n\cdot(n+1)}{2}\}}</math>


Linia 197: Linia 197:
  y := 0;
  y := 0;
  <math>{\color{Red}\{n \geq 0 \land x = 1 \land y = 0\}}</math>
  <math>{\color{Red}\{n \geq 0 \land x = 1 \land y = 0\}}</math>
      <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 1 </span>
    <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 1 </span>
  <math>{\color{Red}\{N\}}</math>
  <math>{\color{Red}\{N\}}</math>
  while  <math>{\color{Red}\{N\}}</math>  x <= n do
  while  <math>{\color{Red}\{N\}}</math>  x <= n do
Linia 229: Linia 229:


  <math>{\color{Red}\{n \geq 1\}}</math>
  <math>{\color{Red}\{n \geq 1\}}</math>
      <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 1 </span>
    <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 1 </span>
  <math>{\color{Red}\{N[y \mapsto 0][x \mapsto 1]\}}</math>
  <math>{\color{Red}\{N[y \mapsto 0][x \mapsto 1]\}}</math>
  x := 1;  
  x := 1;  
Linia 241: Linia 241:


  <math>{\color{Red}\{n \geq 1\}}</math>
  <math>{\color{Red}\{n \geq 1\}}</math>
      <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 1 </span>
    <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 1 </span>
  <math>{\color{Red}\{N[y \mapsto 0][x \mapsto 1]\}}</math>
  <math>{\color{Red}\{N[y \mapsto 0][x \mapsto 1]\}}</math>
  x := 1;  
  x := 1;  
Linia 249: Linia 249:
  (
  (
   <math>{\color{Red}\{N \land x \leq n\}}</math>
   <math>{\color{Red}\{N \land x \leq n\}}</math>
        <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 2 </span>
      <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 2 </span>
   <math>{\color{Red}\{N[x \mapsto x{+}1][y \mapsto y{+}x]\}}</math>
   <math>{\color{Red}\{N[x \mapsto x{+}1][y \mapsto y{+}x]\}}</math>
   y := y + x;
   y := y + x;
Linia 257: Linia 257:
  )
  )
  <math>{\color{Red}\{N \land x > n\}}</math>
  <math>{\color{Red}\{N \land x > n\}}</math>
      <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 3 </span>
    <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 3 </span>
  <math>{\color{Red}\{y=\frac{n\cdot(n+1)}{2}\}}</math>
  <math>{\color{Red}\{y=\frac{n\cdot(n+1)}{2}\}}</math>


Linia 449: Linia 449:
\frac{{\color{Red}\{\beta\}} I {\color{Red}\{\beta\}}
\frac{{\color{Red}\{\beta\}} I {\color{Red}\{\beta\}}
       \quad
       \quad
       {\color{Red}\{\beta \land \neg b\}}</math> I {\color{Red}\{\beta\}}}
       {\color{Red}\{\beta \land \neg b\}} I {\color{Red}\{\beta\}}}
     {{\color{Red}\{\beta\}} \mathbf{repeat}\, I \,\mathbf{until}\, b {\color{Red}\{\beta \land b\}}}
     {{\color{Red}\{\beta\}} \mathbf{repeat}\, I \,\mathbf{until}\, b {\color{Red}\{\beta \land b\}}}
</math>
</math>

Wersja z 08:19, 14 sie 2006


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: 


{n≥1}
x := 1; y := 0;
while x <= n do
  y := y + x;
  x := x + 1
{y=n⋅(n+1)2}


Rozwiązanie

{{{3}}}


Ćwiczenie 2

Uzupełnij poniższe reguły:

?{α}x:=e{β}

?{α}𝐰𝐡𝐢𝐥𝐞b𝐝𝐨I{β}


Rozwiązanie

{{{3}}}


Ćwiczenie 3 (potęgowanie binarne)

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


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


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

Rozwiązanie

{{{3}}}


Ćwiczenie 4

Zaproponuj regułe dla instrukcji 𝐫𝐞𝐩𝐞𝐚𝐭I𝐮𝐧𝐭𝐢𝐥b.


Rozwiązanie

{{{3}}}


Zadania domowe

Ćwiczenie 1

Wyprowadź ostatnią regułę dla pętli 𝐫𝐞𝐩𝐞𝐚𝐭 z pierwszej reguły.


Ćwiczenie 2

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


Ćwiczenie 3

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


{x≥0}
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;
{(b−1)3≤x<b3}


Wskazówka

(m+1)3=m3+3⋅m2+3⋅m+1

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