On 08.07.2012 17:23, Stanislav Maslovski wrote: > On Thu, Jul 05, 2012 at 08:20:19PM +0400, "Артём Н." wrote: >> 04.07.2012 09:21, Stanislav Maslovski пишет: >>> Если система обладает неограниченной памятью, как машина Тьюринга с >>> бесконечной >>> лентой, то в общем случае нельзя. На практике нельзя уже при сколько-нибудь >>> значительном объёме памяти, просто в силу потребного времени. >> Я про практику. > На практике ситуация такова: случаев, где возможно *полное* формальное > доказательство правильности программы *больше*, чем случаев, где для этого > достаточно *простых* тестов. > Как правило, построение *полного* теста эквивалентно решению исходной > программной задачи, и, поэтому, не имеет никакой ценности для доказательства. Понятно. А вообще, случаев, когда: 1. возможно полное доказательство; 2. доказательство имеет практическое значение; много?
>>> На самом деле, он просто утверждает, что тестирование на примерах (т.е., >>> твоё "перечисление всех состояний, подав на вход все комбинации нулей и >>> единиц") ничего не гарантирует. >> Всех состояний - гарантирует. Но это практически невозможно :-) > Да нет же. Почему - следует из вышенаписанного. В частном случае, если представить программу, как конечный автомат с памятью... >>> Можно 1000 раз успешно прогнать *все* >>> комбинации входных переменных некой процедуры, а на 1001-м получить >>> ошибку, например, из-за утечки памяти, или из-за переполнения какой-нибудь >>> переменной-счётчика, которая не обнуляется между вызовами, и т.п. >> Значит не были протестированы _все_ состояния. > Задолбал! :) Не, ну я здесь прав. ;-) > >>> Похоже, что ты сам запутался в своих рассуждениях: тебя *принципиальная* >>> доказуемость интересует, или всё же доказуемость в частных случаях? С >>> первым всё ясно, а про второе тебе уже писали, что доказывать во многих >>> случаях можно, для этого есть методы, и методы эти не основаны на >>> переборе всех нулей и единиц. >> Я неправильно выразился. Полное доказательство корректности достаточно >> сложной >> системы провести на практике невозможно ввиду слишком больших затрат >> ресурсов (и >> ещё возможно, из-за отсутствия метода доказательства). Так? > Нет. Я утверждал, что во многих случаях *полное* формальное > доказательство *возможно* с конечными ресурсами и за конечное время. > Просто это доказательство строится совсем не тем способом, который ты > себе представляешь. Каким? > Вот тебе элементарный пример: докажи теорему Пифагора *тестами* =) Возможно повысить уверенность в том, что алгоритм доказательства теоремы реализован правильно, используя тесты. Про "доказательство" тестами я ничего не писал. :-) >>>> И на практике: будь всё так хорошо, как вы пишите, все бы уже давно писали >>>> на >>>> Прологе (по крайней мере, знали бы что это такое). :-) >>> Незнание, как говорится, не освобождает от ответственности. Плюс, в >>> идеальном мире все бы уже давно писали хотя бы на том же Haskell... >> Что такое "идеальный мир", в данном случае? o.O > Мир, в котором невежество не выставляется за геройство ;) Сомнительная утопия или даже антиутопия... Кстати, а что насчёт Ада? Пишут (в сегодня почившей вики): "Сторонники Ады утверждают, что единственная альтернатива большому и сложному языку в больших проектах — это применение нескольких компактных языков, неизбежно порождающее проблемы с совместимостью, для избавления от которых и была придумана Ада. Они замечают также, что представление о сложности разработки на Аде верно лишь отчасти: написание простой программы на Аде действительно требует больше времени, чем на других, менее формальных языках, типа Си, но отладка и сопровождение программ, особенно крупных и сложных, значительно упрощается. По утверждению Стефена Цейгера из Rational Software Corporation[6], разработка программного обеспечения на Аде в целом обходится на 60 % дешевле, а разработанная программа имеет в 9 раз меньше дефектов, чем при использовании языка Си." Плюс есть GNAT и среда GPS. А от проблем, которые были у старых версий (в т.ч. совместимостью с др. языками), Ada95, вроде как ушёл... И синтаксис с парадигмой знакомые... И пишут на нём. Что про него можете сказать? -- 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/4ffc6bfe.2010...@yandex.ru
