W dniu sobota, 28 marca 2015 10:54:16 UTC+1 użytkownik M.M. napisał:
> > >
> > > 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,
> Właśnie, tego nie da się udowodnić, a jest to też ważny aspekt
> programu. A w testach tak się robi, porównuje się kilka
> różnych algorytmów dla różnych danych.

To, że "nie istnieje w ramach określonego rozmiaru >>lepszy<< program"
jest "ważnym aspektem programu"? Dla kogo jest to ważne? Klienta
interesuje, żeby program działał zadowalająco dobrze, a nie to, żeby
"w ramach określonego rozmiaru programu nie istniał jakiś lepszy".
(W każdym razie ja nie spotkałem nigdy klienta o tak osobliwych
zainteresowaniach. Ale nawet gdybym spotkał, pewnie po prostu nie
uwierzyłbym własnym uszom)
Nie widzę też, w jaki sposób testy miałyby tu być pomocne.

> > tylko nieprecyzyjnej
> > specyfikacji. Co to znaczy,że "w ramach określonego rozmiaru program
> > jest lepszy od innego programu"?
> Zakładamy że specyfikacja jest dobra. To jest kwestia jakości
> użytych algorytmów/heurystyk.

To, co piszesz, nic nie wyjaśnia.
Powiedzenie, że coś jest najlepsze, jest po prostu powiedzeniem
nieprecyzyjnym. Co to znaczy "najlepsze"? Że przynosi najwięcej
pieniędzy? Że ma najwięcej użytkowników? Że najbardziej podoba
się klientowi?
Jeżeli podajesz jawnie złą specyfikację, to potem nie możesz mówić
"zakładamy, że specyfikacja jest dobra", bo nie jest.

> > 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),
> Nie słyszałem o logice temporalnej. Może się mylę, ale to się
> wydaje łatwe. Dla mnie taki dowód sprowadza się do tego, aby
> wszystkie pary kodu, który może wykonać się równolegle, były
> opatrzone semaforami w tej samej kolejności w sensie wykonania i
> w odwrotnej kolejności (też w sensie wykonania).

Mylisz się z pewnością, choćby dlatego, że semafor nie jest jedynym
mechanizmem synchronizującym używanym w programach wielowątkowych.