On 25/03/2015 20:05, j...@p...onet.pl wrote:
>> A zleceniodawca wymaga formalnego dowodu poprawności programu?
>
> nie wymaga, ale jeśli mój algorytm będzie niepoprawny to zostanie
> poważnie naruszona reputacja jego firmy

Nie znam się na algorytmach i ich dowodzeniu, ale mogę powiedzieć tyle,
że normalną praktyką w przemyśle jest testowanie a nie dowodzenie, bo
dowodzenie jest bardzo kosztowne - jest uważane za nieopłacalne nawet
tam, gdzie wchodzą w grę wielomilionowe straty (np. w finansach), a
zaczyna się je stosować AFAIK gdzieś w okolicach oprogramowania pojazdów
kosmicznych - duże potencjalne straty, stosunkowo mała liczba linii kodu.

Poprawność programu praktycznie nigdy nie jest kwestią 100% pewności a
zawsze jest kwestią zarządzania ryzykiem. Zawsze jest pewne
prawdopodobieństwo, że program zawiedzie powodując jakieś straty - nawet
jeśli formalnie udowodniłeś jego poprawność - i zawsze jest pytanie, ile
czasu, pieniędzy i innych zasobów można poświęcić, żeby to ryzyko o
ileśtam zredukować.

Trochę piszę oczywistości, ale piszę to dlatego, że skoro twój
zleceniodawca wymaga, żebyś robił to sam, to być może inne względy
(zachowanie tajemnicy? koszty?) są dla niego ważniejsze niż ryzyko
utraty reputacji na wskutek błędnego działania programu. Druga możliwość
jest oczywiście taka, że nie jest tego świadomy.