Euklides

Naszym celem jest analiza algorytmu Euklidesa i zbadanie jak mozna udowodnić jego poprawność.

Wprowadzenie

W wielu książkach możesz przeczytać dowód poprawnośći algorytmu Euklidesa. Zazwyczaj dowód wykorzystuje zasadę minimum. ... Najkrócej rzecz ujmując dowodzi się, że w standardowej strukturze liczb naturalnych obliczenie algorytmu jest skończone. Mozna zapytać z jakich aksjomatów liczb naturalnych korzysta taki dowód? I tu sprawa sie komplikuje. Bowiem, każdy zestaw aksjomatów dla struktury licb naturalnych ma modele niestandardowe oprócz standardowego modelu liczb naturalnych. W nowszych językach programowania (np. Java) programista może korzystać ze zmiennych typu integer (Nie wchodzimy tu na razie w rozważania co się rozumie przez typ integer). Można także korzystac z typu Integer - różnica formalnie to tylko wielkość litery I, ale Typ Integer jest opisany w deklaracji klasy

call Integer { }

Skąd wiemy jakie własnośći ma zbiór obiektów klasy Integer? Właściciel języka Java nie zdradza nam swoich tajemnic.

Możemy sami zadeklarować klasę integer. Czy nie narobimy sobie kłopotów? Może się tak stać i jest jednym z naszych celów by to uwidocznić.