Удовлетворяет ли программа заданной спецификации?
Я читал несколько статей о зависимых типах и контрактах программирования. Из большей части того, что я прочитал, кажется, что контракты - это динамически проверяемые ограничения, а зависимые типы проверяются статически. Были некоторые бумаги, которые заставили меня думать, что возможно иметь...
Я самостоятельно изучаю формальные методы. Я слышал, что формальные методы используются (и обычно используются только) для создания критически важных программ (таких как контроллер ядерного реактора, контроллер полета самолета, контроллер космического зонда). Вот почему мне интересно узнать это: p...
Усилия по проверке компилятора часто сводятся к тому, чтобы доказать, что компилятор полностью абстрактен: он сохраняет и отражает (контекстуальные) эквивалентности. Вместо того, чтобы предоставлять полные доказательства абстракции, некоторые недавние (основанные на категориях) работы по проверке...
Вопрос: Предположим, у меня есть спецификация задачи, состоящей из аксиом и цели (т. Е. Связанная проблема доказательства состоит в том, является ли цель выполнимой при всех аксиомах). Предположим также, что проблема не содержит каких-либо противоречий / противоречий между аксиомами. Есть ли способ...
Если вы знакомы с проверкой программы, вы, скорее всего, предпочтете прочитать Вопрос перед тем, как начать . Если вы не знакомы с проверкой программы, возможно, вы все равно сможете ответить на этот вопрос, но, скорее всего, вы предпочтете сначала прочитать справочную информацию . Фон Часто...
Семантика большого подмножества OCaml, называемого OCamllight , была формализована в HOL Оуэнсом несколько лет назад. Совсем недавно теоретическая семантика типов меньшего подмножества OCaml была реализована в Nuprl Крейцем, Хейденом и Хикки . Есть ли похожие разработки в...
Я обнаружил, что маркированные переходные системы являются хорошей моделью для моего приложения, а именно есть статья о моделировании вариантов использования с использованием LTS. Вопрос в том, что можно легко доказать о LTS? Я хотел бы повторно использовать существующие решения, чтобы увидеть,...
В монадической логике первого порядка, также известной как монадический класс задачи решения, все предикаты принимают один аргумент. Аккерманн показал, что он может быть разрешен и НЕОБХОДИМО завершен . Однако такие проблемы, как SAT и SMT, имеют быстрые алгоритмы их решения, несмотря на...
Возможно, основным источником проблем с производительностью в Haskell является случай, когда программа по неосторожности создает поток неограниченной глубины - это вызывает как утечку памяти, так и потенциальное переполнение стека при оценке. Классический пример - определение sum = foldr (+) 0в...
Поскольку ответа не было дано, был установлен флаг с просьбой преобразовать этот вопрос в вики сообщества. Комментарии Аарона Стерлинга, Сашо Николова и Вора были объединены в следующую резолюцию, которая открыта для обсуждения в вики сообщества: Решено: Что касается классических алгоритмов,...
В классической статье PLDI'98 Necula «Разработка и реализация сертифицирующего компилятора» верификатор высокого уровня использует: VCGen для генерации условий проверки (предикаты безопасности) Доказательство логической теоремы первого порядка для доказательства условий LF proof checker для...