Re: Несколько вопросов вразброс
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, например.
> На таких языках можно писать программы, которые сами же являются
> доказательствами своей правильности.
Да, кстати, Пролог я не понимаю. :-(
Изначально - всё просто. Затем, правила становятся какие-то дикие (к тому месту,
где начинается рекурсия и прочее). Хотя, может, в книжке было плохо описано.
Но почему программа является априори правильной?
Ведь она там - просто набор отношений, а "Пролог" - система вывода.
Кто сказал, что данный набор отношений будет давать верный с точки зрения
условий задачи результат на любом подмножестве входных данных?
И на практике: будь всё так хорошо, как вы пишите, все бы уже давно писали на
Прологе (по крайней мере, знали бы что это такое). :-)
Reply to: