poprawność semantyczna - algorytm euklidesa

Chuleta
Użytkownik
Użytkownik
Posty: 15
Rejestracja: 3 lis 2009, o 19:57
Płeć: Kobieta
Lokalizacja: Cacerola

poprawność semantyczna - algorytm euklidesa

Post autor: Chuleta »

Udowodnij, że algorytm Euklidesa jest poprawny semantycznie względem warunku początkowego \(\displaystyle{ \left\{\alpha :m>0, n>0\right\}}\) i warunku końcowego \(\displaystyle{ \left\{\beta :a=NWD(a,b)\right\}}\). Niezmiennik pętli:\(\displaystyle{ \left\{\gamma :a>0, b>0, NWD(m,n)=NWD(a,b)\right\}}\).

EUKLIDES-ODEJMOWANIE(m,n:INTEGER)
1 \(\displaystyle{ a \leftarrow m; b \leftarrow n;}\)
2 while a<>b
3 do if a>b
4 then \(\displaystyle{ a \leftarrow a-b}\)
5 else \(\displaystyle{ b \leftarrow b-a}\)
6 return a


Niestety zupełnie nie wiem jak się za to zabrać... będę bardzo wdzięczna za pomoc w rozwiązaniu tego zadania, ponieważ mam jeszcze kilka tego typu zadań do zrobienia i byłoby miło mieć przykładowe rozwiązanie Pozdrawiam!
miodzio1988

poprawność semantyczna - algorytm euklidesa

Post autor: miodzio1988 »

No to robimy to tak:
1) Patrzymy czy niezmiennik jest prawdziwy przed wejściem do pętli
2) Zakladamy, że niezmiennik jest prawdziwy po n obrotach i patrzymy co się dzieje dla n+1 obrotu
(taka indukcja). Czyli robisz założenie, że niezmiennik jest prawdziwy i aptrzysz się co się dzieje gdy jeszcze raz przejdziemy przez pętlę
2a) jesli trzeba sprawdzac rozne przypadki-robisz to
3)Patrzymy co się dzieje gdy wychodzimy z pętli i wychodzi nam warunek koncowy

Możesz też sprawdzić czy wszystkie operacje są tutaj okreslone rowniez oraz sprawdzic wlasnosc "stopu"-chociaz Twoje zadanie nie wymaga tego.
ODPOWIEDZ