Wstęp do programowania/Wstęp do algorytmów/Ćwiczenia: Różnice pomiędzy wersjami

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Aneczka (dyskusja | edycje)
Aneczka (dyskusja | edycje)
Linia 75: Linia 75:
Skoro testowanie nie daje pewności, że mamy dobry program to potrzebujemy innego narzędzia, które pozwoli nam spać spokojnie - możemy (przynajmniej teoretycznie) dowieść formalnie poprawność programu.  
Skoro testowanie nie daje pewności, że mamy dobry program to potrzebujemy innego narzędzia, które pozwoli nam spać spokojnie - możemy (przynajmniej teoretycznie) dowieść formalnie poprawność programu.  
Powinniśmy ustalić co jest formalną specyfikacją naszego zadania (W = A ∩ B) i zrobić formalny dowód, że dla każdego punktu p zdanie p ε A ∩ B jest równoważne temu, że p ε W. Teraz już możemy spać spokojnie - nasz algorytm '''jest''' poprawny (o ile nie pomylilismy się w dowodzie)!
Powinniśmy ustalić co jest formalną specyfikacją naszego zadania (W = A ∩ B) i zrobić formalny dowód, że dla każdego punktu p zdanie p ε A ∩ B jest równoważne temu, że p ε W. Teraz już możemy spać spokojnie - nasz algorytm '''jest''' poprawny (o ile nie pomylilismy się w dowodzie)!
<div class="mw-collapsible mw-made=collapsible mw-collapsed">
 
'''Dowód''' 
{{dowod||dowod_1|<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">  
<div class="mw-collapsible-content" style="display:none">  
Najpierw zauważmy, że  
Najpierw zauważmy, że  
  p &epsilon; A &cap; B  wtedy i tylko wtedy    p.x &epsilon; rzutX(A) &cap; rzutX(B) i p.y &epsilon; rzutY(A) &cap; rzutY(B)  
  p &epsilon; A &cap; B  wtedy i tylko wtedy    p.x &epsilon; rzutX(A) &cap; rzutX(B) i p.y &epsilon; rzutY(A) &cap; rzutY(B)  
Linia 96: Linia 95:
W drugą stronę dowód przebiega podobnie. Ponieważ  p.x &epsilon; rzutX(W) to max(A.x1,B.x1)  &le; p.x &le; min(A.x2,B.x2). Stąd A.x1 &le; p.x &le; A.x2  a więc p.x &epsilon; rzutX(A). I tak samo dla B. A więc p.x &epsilon; rzutX(A) &cap; rzutX(B).  
W drugą stronę dowód przebiega podobnie. Ponieważ  p.x &epsilon; rzutX(W) to max(A.x1,B.x1)  &le; p.x &le; min(A.x2,B.x2). Stąd A.x1 &le; p.x &le; A.x2  a więc p.x &epsilon; rzutX(A). I tak samo dla B. A więc p.x &epsilon; rzutX(A) &cap; rzutX(B).  
</div>
</div>
</div>
</div>}}
 
Najważniejszy morał z tego zadania, to pochwała myślenia - trzeba wykonać dużo pracy (myślowej) zanim zacznie się pisać pierwszy wiersz programu/algorytmu.
Najważniejszy morał z tego zadania, to pochwała myślenia - trzeba wykonać dużo pracy (myślowej) zanim zacznie się pisać pierwszy wiersz programu/algorytmu.



Wersja z 10:11, 1 sie 2006

Zadanie 1

Podaj algorytm wyliczający część wspólną dwóch zadanych prostokątów o bokach równoległych do osi układu współrzędnych.

Analiza specyfikacji

  • Czy specyfikacja podana w zadaniu jest wystarczająca do zapisania algorytmu ?

Odpowiedź

{{{2}}}
  • Co może być częścią wspólną ?

Odpowiedź

{{{2}}}
  • Jaka może być postać danych ?

Odpowiedź

{{{2}}}
  • Jaka może być postać wyniku ?

Odpowiedź

{{{2}}}

Znajdowanie algorytmu

Gdy zaczniemy analizować możliwe wzajemne położenia prostokątów okaże się, że przypadków jest co najmniej kilkanaście.

Wskazówka 1

{{{3}}}

Wskazówka 2

{{{3}}}

Rozwiązanie

{{{3}}}

Testowanie

Mając algorytm/program powinniśmy go przetestować, czyli sprawdzić jakie daje wyniki dla przykładowych danych. Warto testować z jednej strony przypadki typowe, z drugiej zaś szczególne przypadki graniczne (np. prostokąty dotykające się jednym rogiem lub jeden prostokąt zawarty w drugim). Testowanie jest ważne i trzeba je robić, mimo że, w przypadku gdy nie wykryje błędów, nic nie daje (nawet nie mamy pewności, że dla przetestowanych danych zawsze dostaniemy poprawny wynik, bo np. mamy niezainicjalizowane zmienne).

Dowód poprawności

Skoro testowanie nie daje pewności, że mamy dobry program to potrzebujemy innego narzędzia, które pozwoli nam spać spokojnie - możemy (przynajmniej teoretycznie) dowieść formalnie poprawność programu. Powinniśmy ustalić co jest formalną specyfikacją naszego zadania (W = A ∩ B) i zrobić formalny dowód, że dla każdego punktu p zdanie p ε A ∩ B jest równoważne temu, że p ε W. Teraz już możemy spać spokojnie - nasz algorytm jest poprawny (o ile nie pomylilismy się w dowodzie)!

Dowód

{{{3}}}

Najważniejszy morał z tego zadania, to pochwała myślenia - trzeba wykonać dużo pracy (myślowej) zanim zacznie się pisać pierwszy wiersz programu/algorytmu.

Inna wersja zadania

A co by było gdyby prostokąty były otwarte (czyli bez brzegu) ?

Reprezentacja używana powyżej jest nadal dobra zarówno dla danych jak i dla wyniku. Tym razem możliwe są tylko dwie postacie wyniku: albo prostokąt (z wnętrzem) o bokach równoległych do osi układu, albo zbiór pusty. Algorytm który podaliśmy powyżej działa również dla prostokątów otwartych; w dowodzie poprawności trzeba by jedynie zamienić nierówności nieostre (≤, ≥) na ostre (<, >).

Zadanie 2

Podaj algorytm wyliczający najmniejszy prostokąt o bokach równoległych do osi układu współrzędnych zawierający dwa zadane prostokąty o bokach równoległych do osi układu współrzędnych.

Wskazówka

Rozwiązanie

Zadanie 3

Używając tylko czterech podstawowych działań arytmetycznych sprawdź czy dwa odcinki na płaszczyźnie, zadane porzez współrzędne końców, przecinają się.

Wskazówka 1

Wskazówka 2

Wskazówka 3

Rozwiązanie

Zadanie 4

Sprawdż czy dane dwa równolełoboki na płaszczyźnie przecinają się. Równoległoboki mają boki dowolnie nachylone do osi współrzędnych i zadane są porzez współrzędne czterech rogów podanych zgodnie z ruchem wskazówek zegara.

Wskazówka 1

Rozwiązanie