W dniu sobota, 28 marca 2015 05:04:04 UTC+1 użytkownik M.M. napisał:

> > W takim razie zgoda -- tego rodzaju "poprawność" jest niemożliwa do uzyskania.
> > Należy jednak mieć na uwadze, że z formalnego punktu widzenia poprzez
> > "poprawność" dowodu rozumie się to, czy każdy krok jest zgodny z regułami,
> > natomiast w tym przypadku raczej należałoby użyć słowa "adekwatność"
> > (na przykład teza Churcha-Turinga postuluje adekwatność maszyny Turinga
> > jako modelu ujmującego intuicyjne rozumienie obliczalności)
>
> Mój (hipotetyczny) klient zamawia najlepszy program do gry w
> szachy o łącznym rozmiarze kodu i danych nie większym niż 1MB. Napisałem
> taki program. Jak mam przeprowadzić dowód, że nie istnieje w
> ramach tego rozmiaru lepszy program?

To akurat nie jest problem metody dowodowej, tylko nieprecyzyjnej
specyfikacji. Co to znaczy,że "w ramach określonego rozmiaru program
jest lepszy od innego programu"?

Zresztą cechy użytkowe nie są czymś, co dowodzi się formalnie
(bo są subiektywne). Formalnie chcemy dowodzić raczej pewnych
inwariantów -- że na przykład w programie wielowątkowym nie dojdzie
do sytuacji dead-locku (klasyczne zastosowane logik temporalnych),
że dla określonej klasy danych wejściowych program się zatrzyma,
że zużycie zasobów w czasie działania programu będzie ograniczona
określoną funkcją od czasu działania i rozmiaru danych wejściowych
itd.