Вопросы с тегом «software-verification»

66
Формальная проверка программы на практике

Как инженер-программист, я пишу много кода для промышленных продуктов. Относительно сложные вещи с классами, потоками, некоторыми проектными усилиями, но также и некоторыми компромиссами для производительности. Я много тестирую, и я устал от тестирования, поэтому я заинтересовался инструментами...

23
Алгоритм решения «проблемы остановки» Тьюринга

Этот вопрос был перенесен из теоретического обмена стеков информатики, потому что на него можно ответить в обмене стеков информатики. Мигрировал 7 лет назад . «Алан Тьюринг доказал в 1936 году, что общий алгоритм для решения проблемы остановки для всех возможных пар ввода программы не может...

18
Как проверить, возвращают ли два алгоритма один и тот же результат для любого ввода?

Как проверить, возвращают ли два алгоритма (скажем, сортировка слиянием и наивная сортировка) один и тот же результат для любого входа, когда набор всех входов бесконечен? Обновление: Спасибо, Бен, за описание того, как это невозможно сделать алгоритмически в общем случае. Ответ Дейва - это краткое...

17
Правильность программы, спецификация

Из Википедии: В теоретической информатике правильность алгоритма утверждается, когда говорят, что алгоритм корректен по отношению к спецификации. Но проблема в том, что получить «подходящую» спецификацию - это не тривиальная задача, и нет 100% правильного метода (насколько я знаю), чтобы получить...

12
Почему мы больше не исследуем гарантии времени компиляции?

Мне нравится все, что происходит во время компиляции, и мне нравится идея, что, как только вы скомпилируете программу, вы получите много гарантий относительно ее выполнения. Вообще говоря, статическая система типов (Haskell, C ++, ...), похоже, дает более сильные гарантии во время компиляции, чем...

11
Как обращаться с массивами во время корректных проверок в стиле Хоара

В дискуссии вокруг этого вопроса Жиль правильно упоминает, что любое доказательство правильности алгоритма, использующего массивы, должно доказывать, что нет доступа к массиву вне пределов; в зависимости от модели времени выполнения это может вызвать ошибку времени выполнения или доступ к...

10
Каковы общие формальные методы для проверки правильности функционального кода?

Я хочу предоставить доказательства для частей программы на Haskell, которую я пишу, как часть моей диссертации. Однако до сих пор мне не удалось найти хорошую справочную работу. Вступительная книга Грэма Хаттона « Программирование на Haskell» ( Google Books ), которую я читаю, изучая Haskell,...

9
Введение в проверку логики первого порядка

Я пытаюсь научить себя различным подходам к проверке программного обеспечения. Я прочитал несколько статей. Насколько я узнал, логика высказываний с темпоральным обычно использует проверку моделей с помощью решателей SAT (в текущих - реактивных системах), но как насчет логики первого порядка с...

9
Могут ли методы проверки программы предотвратить появление ошибок жанра Heartbleed?

На вопрос об ошибке Heartbleed Брюс Шнайер написал в своей «Крипто-грамме» от 15 апреля: «Катастрофический» - правильное слово. По шкале от 1 до 10 это 11 '. Несколько лет назад я читал, что ядро ​​определенной операционной системы строго проверено современной системой проверки программ....