On Thu, Jul 05, 2012 at 08:20:19PM +0400, "Артём Н." wrote: > 04.07.2012 09:21, Stanislav Maslovski пишет: > > Если система обладает неограниченной памятью, как машина Тьюринга с > > бесконечной > > лентой, то в общем случае нельзя. На практике нельзя уже при сколько-нибудь > > значительном объёме памяти, просто в силу потребного времени. > Я про практику.
На практике ситуация такова: случаев, где возможно *полное* формальное доказательство правильности программы *больше*, чем случаев, где для этого достаточно *простых* тестов. Как правило, построение *полного* теста эквивалентно решению исходной программной задачи, и, поэтому, не имеет никакой ценности для доказательства. > > На самом деле, он просто утверждает, что тестирование на примерах (т.е., > > твоё "перечисление всех состояний, подав на вход все комбинации нулей и > > единиц") ничего не гарантирует. > Всех состояний - гарантирует. Но это практически невозможно :-) Да нет же. Почему - следует из вышенаписанного. > > Можно 1000 раз успешно прогнать *все* > > комбинации входных переменных некой процедуры, а на 1001-м получить > > ошибку, например, из-за утечки памяти, или из-за переполнения какой-нибудь > > переменной-счётчика, которая не обнуляется между вызовами, и т.п. > Значит не были протестированы _все_ состояния. Задолбал! :) > > Похоже, что ты сам запутался в своих рассуждениях: тебя *принципиальная* > > доказуемость интересует, или всё же доказуемость в частных случаях? С > > первым всё ясно, а про второе тебе уже писали, что доказывать во многих > > случаях можно, для этого есть методы, и методы эти не основаны на > > переборе всех нулей и единиц. > Я неправильно выразился. Полное доказательство корректности достаточно сложной > системы провести на практике невозможно ввиду слишком больших затрат ресурсов > (и > ещё возможно, из-за отсутствия метода доказательства). Так? Нет. Я утверждал, что во многих случаях *полное* формальное доказательство *возможно* с конечными ресурсами и за конечное время. Просто это доказательство строится совсем не тем способом, который ты себе представляешь. Вот тебе элементарный пример: докажи теорему Пифагора *тестами* =) > >>> Например, существуют языки программирования, которые вычисляют через > >>> доказательство (через формальную процедуру вывода). PROLOG, например. > >>> На таких языках можно писать программы, которые сами же являются > >>> доказательствами своей правильности. > >> Да, кстати, Пролог я не понимаю. :-( > >> Изначально - всё просто. Затем, правила становятся какие-то дикие (к тому > >> месту, > >> где начинается рекурсия и прочее). Хотя, может, в книжке было плохо > >> описано. > >> Но почему программа является априори правильной? > > Я такого не утверждал. Что я утверждал, отквочено выше. > А, кажется понял. :-) Примерно: "Программа существует и выдаёт правильные > результаты, значит является правильной"? O_O > > Никто не сказал, однако: > > Чем ближе язык программирования по синтаксису и семантике к формальному > > описанию задачи, тем проще на нем написать верную программу. В случае > > пролога, текст программы просто перефразирует исходное условие на языке > > логики предикатов. Т.е., программа получается автоматически верной, если > > условие задачи было успешно выражено на языке формальной логики и затем > > записано в синтаксисе пролога. По сути, это всё, что требуется. Меньше > > уже нельзя, без наделения машины интеллектом и знаниями о внешнем мире. > Хм... Но это тоже самое. Просто программа - это описание. И язык здесь - > логика > предикатов. Проверка нужна для описания. Для проверки его соответствия условию > задачи. В сущности, это такая же программа, только "перевёрнутая". И, > соответственно, требует проверки. Так? Ты явно хочешь свернуть с доказательства правильности *решения* задачи на доказательство правильности *постановки* задачи. Это отдельная проблема, которая формальными методами не решается *в принципе*. > >> И на практике: будь всё так хорошо, как вы пишите, все бы уже давно писали > >> на > >> Прологе (по крайней мере, знали бы что это такое). :-) > > Незнание, как говорится, не освобождает от ответственности. Плюс, в > > идеальном мире все бы уже давно писали хотя бы на том же Haskell... > Что такое "идеальный мир", в данном случае? o.O Мир, в котором невежество не выставляется за геройство ;) -- Stanislav -- 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/20120708132346.GC18653@kaiba.homelan
