03.07.2012 01:14, Stanislav Maslovski пишет: > On Mon, Jul 02, 2012 at 08:36:58PM +0400, "Артём Н." wrote: >> 02.07.2012 19:42, Artem Chuprina пишет: >>> Артём Н. -> debian-russian@lists.debian.org @ Mon, 02 Jul 2012 19:13:04 >>> +0400: >>> >>> >> >> АН> Хм... Да, пожалуй, это верно. >>> >> >> АН> Но, если система выполняет ответственные действия..? >>> >> >> АН> Вопрос в том совместить требования надёжности и корректности с >>> >> >> АН> отказоустойчивостью и возможностью восстановления после сбоя? >>> >> >> Кодогенерация сишного или даже ассемблерного кода на какой-нибудь >>> agda. >>> >> >> Которая из тебя душу вынет, пока ты ей корректность не докажешь. >>> >> >> Правда, порог вхождения весьма высокий. >>> >> АН> Про Agda не слышал. Что-то небогато по ней документации, но, >>> >> АН> насколько я понял, это система автоматического доказательства >>> >> АН> теорем. Не очень понимаю, как она может быть использована, в данном >>> >> АН> контексте: тесты же должны выполняться после компиляции..? >>> >> В данном случае компиляция выполняется вместо тестов. Тесты, в отличие >>> >> от доказательства корректности, не являются гарантией надежности. >>> АН> Но ведь полное доказательство корректности провести невозможно..? >>> Кто сказал? >> Ну это самоочевидно. В крайнем случае, возможно провести доказательство >> корректности отдельно взятой функции, если она минимальна (имеет строго >> определённые области значения и области определения, причём количество таких >> областей ограничено и известный тип зависимостей для этих областей), что >> позволяет доказать корректность, используя определённый набор правил... > Вообще, есть такая теорема Гёделя о неполноте, согласно которой в любой > формальной системе, сводимой в определённом смысле к арифметике, > существуют недоказуемые утверждения. Которая, думаю, сюда не очень подходит: есть набор правил, которые должны выполняться для доказательства непротиворечивости. Т.е., имеются некоторые утверждения от которых возможно отталкиваться. К Гёделю и проблемам Гильберта это отношения не имеет. К счастью. :-D К тому же, в данном частном случае, система, как правило, дискретна. И, в теории, возможно перечислить все её состояния, подав на вход все комбинации "нулей и единиц" (даже, если система с памятью).
На практике - невозможно для сложных систем. > В теории алгоритмов аналог этой теоремы формулируется примерно так: > Не существует алгоритма, позволяющего по описанию произвольного > алгоритма и его исходных данных определить, останавливается ли > этот алгоритм на этих данных (т.е., выдаёт результат) или работает > бесконечно. Ну да, невозможность вывода универсального алгоритма. Там же немного другая задача. > Т.е., общей процедуры доказательства правильности программ в принципе не > существует. Однако, это не означает, что в частных случаях такое > доказательство провести нельзя. Вопрос -то там был изначально в другом. А. Чуприна написал, что: "В данном случае компиляция выполняется вместо тестов. Тесты, в отличие от доказательства корректности, не являются гарантией надежности." Т.е., подразумевал, что в этом случае возможен отказ от тестов. Мне кажется это сомнительным. По причине того, что полное доказательство, в принципе, провести невозможно (в зависимости от уровня сложности, конечно). > Например, существуют языки программирования, которые вычисляют через > доказательство (через формальную процедуру вывода). PROLOG, например. > На таких языках можно писать программы, которые сами же являются > доказательствами своей правильности. Да, кстати, Пролог я не понимаю. :-( Изначально - всё просто. Затем, правила становятся какие-то дикие (к тому месту, где начинается рекурсия и прочее). Хотя, может, в книжке было плохо описано. Но почему программа является априори правильной? Ведь она там - просто набор отношений, а "Пролог" - система вывода. Кто сказал, что данный набор отношений будет давать верный с точки зрения условий задачи результат на любом подмножестве входных данных? И на практике: будь всё так хорошо, как вы пишите, все бы уже давно писали на Прологе (по крайней мере, знали бы что это такое). :-) -- 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/4ff304ad.6010...@yandex.ru
