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

Ответить