On 10 Sie, 21:17, Michoo <m...@v...pl> wrote:

> Ktoś na którejś grupie już poruszał kwestię - opracowano algorytm,
> dowiedziono poprawności po czym okazało się, że algorytm się sypie bo
> rzeczywisty komputer ma skończony zbiór wartości reprezentowanych w int.

W takim razie źle dowiedziono jego poprawności.

Dowodzenie poprawności czegokolwiek powinno się odbywać a) na kodzie
źródłowym (a nie na obrazkach) i b) z uwzględnieniem typów docelowych.
Wtedy nie ma problemów jak powyżej.
Przykładowo, SPARK robi to całkiem sprawnie.

Nie odrzucałbym metod formalnych tylko dlatego, że ktoś kiedyś ich źle
użył.

--
Maciej Sobczak * http://www.inspirel.com