Комментарии 27
А есть формальное доказательство что программа на rust переписанная и верифицированная в coq является верифицированной и на rust ?
1) я думаю что такое доказательство должно быть (но я не пишу на расте :) )
2) иногда код - 100% идеален. Но есть баги в компидяторе, в ОС, в железе. И если вдруг даже всё это работает идельно и безошибочно - иногда прилетают еще космические лучи %)
Разве можно доказать отсутствие?
А если в рамках данной статьи, то даже железное доказательство правильности кода может разбиться об обычный аппаратный сбой в ячейке памяти.
Да. Это просто функция из типа, соответствующего несуществующему объекту, в боттом.
Вы немного лукавите
А вот средствами формальной верификации как раз можно доказывать отсутствие конкретных видов ошибок в коде (ниже мы приведем пример)
Поэтому правильнее будет написать, что:
Формальная верификация — это доказательство с использованием математических методов корректности отсутствия конкретных видов ошибок в программном обеспечении.
Почему?
корректность ПО != отсутствию конкретных видов ошибок
Важно помнить, что не существует средств, дающих больше гарантий.
Статистика (например, результатов тестирования) может дать хоть и не больший, но зато более точный ответ. Причем, с учетом надежности используемого оборудования.
Сразу скажу, что я написал это не для того, чтобы сказать, что формальная верификация ПО не нужна. Нет, конечно нужна! Но это вовсе не панацея от наличия ошибок программах, как бы не хотелось это представить, а всего лишь один из инструментов повышения качества программного кода и не более.
Доказать отсутствие вполне можно. Например, ознакомившись со школьным курсом геометрии, в общем-то по моему вполне можно доказать что нет треугольников с суммой углов больше 180 градусов.
Ну и да, вполне можно доказывать отсутствие ошибок в программах, чем инженеры по формальной верификации и занимаются :).
Объясните, пожалуйста, как формальная верификация (ФВ) сочетается с проблемой остановки. Если в общем случае нельзя даже доказать, что программа не зависнет, то как ФВ вообще работает? Все наши программы принадлежат к какому-то отдельном узкому классу, или что? Спасибо.
Скорее, ФВ не имеет одного универсального алгоритма для проверки любой программы, это лишь набор методов/приёмов/техник, которые применяются в каждом случае по-своему. А в частных случаях и проблема останова разрешима.
Проблема останова — это как вероятность умереть от прямого попадания метеорита, которая не равна нулю, но настолько мала, что ею все пренебрегают. Есть очень узкий класс программ, для которых невозможно определить, завершатся ли они когда-нибудь, который и не позволяет решить проблему останова в общем виде, и широкий класс программ, для которых всё ясно. Я совершенно не удивлюсь, если абсолютно все программы, для которых проблема останова неразрешима, специально созданы именно с целью показать неразрешимость этой проблемы, а не получены в результате решения какой-либо практической задачи.
Системы формальной верификации используют предположение о том, что программа должна за конечный промежуток времени решать поставленную пред ней задачу и люди не пытаются верифицировать то, что верифицировать невозможно в принципе. В этом предположении можно смело заменять утверждение «функция либо выдаст верный результат, либо никогда не завершит свою работу» на утверждение «функция выдаст верный результат».
Я, конечно, не специалист по теории вычислений и могу ошибаться, но мне кажется, что проблема останова — это не про незавершимые вычисления, а про вычисления, про которые невозможно сказать, завершимы они или нет. Для сепулек незавершимость легко доказать, там состояние повторяется спустя несколько итераций. Хорошим примером проблемы останова мне видится программа, которая в десятичном представлении числа √2 (или ещё какой-нибудь непериодической бесконечной дроби) ищет последовательность цифр, переданную на вход, и возвращает её позицию.
Да, и я писала о проблеме останова тут
Объясните, пожалуйста, как формальная верификация (ФВ) сочетается с проблемой остановки.
Пытаемся доказать, что подпрограмма принадлежит к узкому классу. Иногда доказательство не удаётся, иногда это можно исправить подправив подпрограмму.
Если в общем случае нельзя даже доказать, что программа не зависнет, то как ФВ вообще работает?
Более того, есть очень известный класс программ, которые по ТЗ могут выполняться бесконечно долго — диалоговые программы для взаимодействия с пользователем (MS Word, к примеру).
Спасибо за вопрос.
Проверка завершаемости в Coq консервативна. Это означает, что Coq
принимает только функции определенного вида, про которые он точно может
сказать, что эта функция завершается. Речь идет о рекурсивных функциях (Fixpoint). Остальные функции не проходят проверку завершаемости, даже если такая функция на самом деле завершается. Но для функций Fixpoint, Coq требует, чтобы рекурсивные вызовы осуществлялись только на параметрах, которые синтаксически уменьшаются на каждом шаге итерации. Такой парамер Coq как правило может найти сам, его можно также явно указать.
Проверку завершаемости в Coq над функцией можно отключить (установить над ней флажок #[bypass_check(guard)])
Я писала о проблеме остановки в этой статье.
Я писала о проблеме остановки: https://habr.com/ru/articles/749662/
Можно доказать, что программа не зависнет.
Но универсального алгоритма не существует.
Я, пожалуй, дополню ответы выше.
Программы не принадлежат к отдельному узкому классу.
Проблему останова действительно нельзя решить (по крайней мере на устройстве "одного ранга" что ли.. про гипотетические устройства более других "рангов" можно глянуть википедию).
Однако её нельзя решить в общем случае. Для каждого конкретного частного случая её можно попытаться решить. Построенное решение (если удалось его построить, конечно) и есть доказательство завершаемости алгоритма. Те математики которые анализируют алгоритмы, время от времени развлекаются решением проблемы останова (каждый раз в частном случае разумеется). Этим же занимаются и инженеры по формальной верификации.
Чуть более подробно, ситуация такая: для части случаев Coq (и другие подобные системы) может автоматически решать проблему останова. Конкретно Coq определяет что рекурсивный вызов рассматриваемой функции происходит на структурно меньшем аргументе. И если это так, то это значит что алгоритм завершится (поскольку так определяются индуктивные типы в Coq). Но это работает только для примитивно-рекурсивных функций. В общем случае приходится формулировать и доказывать утверждения о завершаемости руками.
Один из подходов к доказательству завершаемости общерекурсивных функций средствами Coq описан у автора в одной из публикаций.
Формально верефицированную программу нужно компилировать формально проверенным компилятором, который скомпилирован формально проверенным компилятором...? Ещё нужно процессор небось формально verified и операционную систему при её наличии.
Ну или всё зависит от задачи?
На практике многие утверждения приходится аксиоматизировать. Что-то остается недоказанным. Что-то приходится допускать. Все те ссылки, что приведены в статье о текущих разработках в сфере ФВ, это исследовательские работы на базе университетов. Компилятор С (проект CompCert) верифицирован не полностью (верифицированы его основные части). Хота, на данный момент, возможно (не уверена), они уже завершили эту работу, и верифицировали оставшиеся блоки.
Я довольно много пробовал всего и моё мнение - пока хорошего пруфчекера нет. И перспективней всех Metamath, если бы там удалось решить проблемы с подстановкой (в Metamath есть только простая подстановка, не заботящаяся о переименовании связанных переменных в случае коллизий, поэтому формализовать логику с кванторами или лямбда-исчисление приходится крайне нестандартными способами). Проблемы эти математические, не программистские.
Публикации
Что такое формальная верификация