Semantyka i weryfikacja programów/Ćwiczenia 15

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania

Zawartość

Ostatnie ćwiczenia poświęcone będa dowodzeniu poprawności całkowitej programów.


Poprawność całkowita

Ćwiczenie 1 (potęgowanie binarne)

Przeprowadź dowód poprawności całkowitej (poprawność częściowa plus własność stopu) potęgowania binarnego:



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


Rozwiązanie


Ćwiczenie 2

Przeprowadź dowód poprawności całkowitej poniższego programu.




s := 1; i := 1;
while i < n do
  k := 1; l := 0; p := 1;
  while p < i do
    k := k + 1;
    if l < p then
      l := l + 1;
      p := 1
    else
      p := p + 1;
  s := s + 6 * k + p - l;
  i := i + 1;
 


Wskazówka


Rozwiązanie (poprawność częściowa)


Rozwiązanie (poprawność calkowita)

Zadania domowe

Ćwiczenie 1

Przeprowadź dowód poprawności całkowitej poniższego programu.



i := 1; j := 2 * n;
while A[i] < A[j] do
  ,,zamień A[i] i A[j]";
  i := i + 1;
  j := j - 1;