On Thursday, March 26, 2015 at 10:29:57 PM UTC+1, Andrzej Jarzabek wrote:
> No to teraz całkowicie bez szydery i na poważnie spytam, jakie są
> praktyczne możliwości. Mam powiedzmy program w C++, kilkaset tysięcy
> linii kodu, korzysta z boosta, wątków, libc, bazy danych, MOM-a itd. -
> co można zrobić żeby udowodnuć jego poprawność i ile to będzie kosztowało?
Myślę że w praktyce w ogóle nie ma możliwości przeprowadzenia takiego
dowodu, nawet dla mniejszych programów. Jak udowodnić, że w dowodzie
nie ma błędu?
Pozdrawiam