04.07.2012 09:21, Stanislav Maslovski пишет: >> К тому же, в данном частном случае, система, как правило, дискретна. >> И, в теории, возможно перечислить все её состояния, подав на вход все >> комбинации >> "нулей и единиц" (даже, если система с памятью). > Если система обладает неограниченной памятью, как машина Тьюринга с > бесконечной > лентой, то в общем случае нельзя. На практике нельзя уже при сколько-нибудь > значительном объёме памяти, просто в силу потребного времени. Я про практику.
>>> Т.е., общей процедуры доказательства правильности программ в принципе не >>> существует. Однако, это не означает, что в частных случаях такое >>> доказательство провести нельзя. >> Вопрос -то там был изначально в другом. >> А. Чуприна написал, что: >> "В данном случае компиляция выполняется вместо тестов. Тесты, в отличие от >> доказательства корректности, не являются гарантией надежности." > Верное утверждение. Согласен. Но вопрос не в том. >> Т.е., подразумевал, что в этом случае возможен отказ от тестов. > На самом деле, он просто утверждает, что тестирование на примерах (т.е., > твоё "перечисление всех состояний, подав на вход все комбинации нулей и > единиц") ничего не гарантирует. Всех состояний - гарантирует. Но это практически невозможно :-) > Можно 1000 раз успешно прогнать *все* > комбинации входных переменных некой процедуры, а на 1001-м получить > ошибку, например, из-за утечки памяти, или из-за переполнения какой-нибудь > переменной-счётчика, которая не обнуляется между вызовами, и т.п. Значит не были протестированы _все_ состояния. >> Мне кажется это сомнительным. >> По причине того, что полное доказательство, в принципе, провести невозможно >> (в >> зависимости от уровня сложности, конечно). > Похоже, что ты сам запутался в своих рассуждениях: тебя *принципиальная* > доказуемость интересует, или всё же доказуемость в частных случаях? С > первым всё ясно, а про второе тебе уже писали, что доказывать во многих > случаях можно, для этого есть методы, и методы эти не основаны на > переборе всех нулей и единиц. Я неправильно выразился. Полное доказательство корректности достаточно сложной системы провести на практике невозможно ввиду слишком больших затрат ресурсов (и ещё возможно, из-за отсутствия метода доказательства). Так? >>> Например, существуют языки программирования, которые вычисляют через >>> доказательство (через формальную процедуру вывода). PROLOG, например. >>> На таких языках можно писать программы, которые сами же являются >>> доказательствами своей правильности. >> Да, кстати, Пролог я не понимаю. :-( >> Изначально - всё просто. Затем, правила становятся какие-то дикие (к тому >> месту, >> где начинается рекурсия и прочее). Хотя, может, в книжке было плохо описано. >> Но почему программа является априори правильной? > Я такого не утверждал. Что я утверждал, отквочено выше. А, кажется понял. :-) Примерно: "Программа существует и выдаёт правильные результаты, значит является правильной"? >> Ведь она там - просто набор отношений, а "Пролог" - система вывода. >> Кто сказал, что данный набор отношений будет давать верный с точки зрения >> условий задачи результат на любом подмножестве входных данных? > Никто не сказал, однако: > Чем ближе язык программирования по синтаксису и семантике к формальному > описанию задачи, тем проще на нем написать верную программу. В случае > пролога, текст программы просто перефразирует исходное условие на языке > логики предикатов. Т.е., программа получается автоматически верной, если > условие задачи было успешно выражено на языке формальной логики и затем > записано в синтаксисе пролога. По сути, это всё, что требуется. Меньше > уже нельзя, без наделения машины интеллектом и знаниями о внешнем мире. Хм... Но это тоже самое. Просто программа - это описание. И язык здесь - логика предикатов. Проверка нужна для описания. Для проверки его соответствия условию задачи. В сущности, это такая же программа, только "перевёрнутая". И, соответственно, требует проверки. Так? >> И на практике: будь всё так хорошо, как вы пишите, все бы уже давно писали на >> Прологе (по крайней мере, знали бы что это такое). :-) > Незнание, как говорится, не освобождает от ответственности. Плюс, в > идеальном мире все бы уже давно писали хотя бы на том же Haskell... Что такое "идеальный мир", в данном случае? o.O -- To UNSUBSCRIBE, email to debian-russian-requ...@lists.debian.org with a subject of "unsubscribe". Trouble? Contact listmas...@lists.debian.org Archive: http://lists.debian.org/4ff5bec3.1080...@yandex.ru
