Re: Несколько вопросов вразброс
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 не слышал. Что-то небогато по ней документации, но,
> > >> АН> насколько я понял, это система автоматического доказательства
> > >> АН> теорем. Не очень понимаю, как она может быть использована, в данном
> > >> АН> контексте: тесты же должны выполняться после компиляции..?
> > >> В данном случае компиляция выполняется вместо тестов. Тесты, в отличие
> > >> от доказательства корректности, не являются гарантией надежности.
> > АН> Но ведь полное доказательство корректности провести невозможно..?
> > Кто сказал?
> Ну это самоочевидно. В крайнем случае, возможно провести доказательство
> корректности отдельно взятой функции, если она минимальна (имеет строго
> определённые области значения и области определения, причём количество таких
> областей ограничено и известный тип зависимостей для этих областей), что
> позволяет доказать корректность, используя определённый набор правил...
Вообще, есть такая теорема Гёделя о неполноте, согласно которой в любой
формальной системе, сводимой в определённом смысле к арифметике,
существуют недоказуемые утверждения.
В теории алгоритмов аналог этой теоремы формулируется примерно так:
Не существует алгоритма, позволяющего по описанию произвольного
алгоритма и его исходных данных определить, останавливается ли
этот алгоритм на этих данных (т.е., выдаёт результат) или работает
бесконечно.
Т.е., общей процедуры доказательства правильности программ в принципе не
существует. Однако, это не означает, что в частных случаях такое
доказательство провести нельзя.
Например, существуют языки программирования, которые вычисляют через
доказательство (через формальную процедуру вывода). PROLOG, например.
На таких языках можно писать программы, которые сами же являются
доказательствами своей правильности.
--
Stanislav
Reply to: