Semantyka i weryfikacja programów/Ćwiczenia 13

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania

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