Логика для проверки программного обеспечения

Question

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

Вопрос в том, какую логику использовать. Две основные позиции выглядят так:

1. Логика первого порядка в порядке.

2. Логика первого порядка недостаточно выразительна, вам нужна логика высшего порядка.

Проблема в том, что обе позиции оказали большую поддержку. Так какой из них прав? Если это второе, есть ли какие-нибудь доступные примеры того, что вы хотите сделать, чтобы у верификаторов, основанных на логике первого порядка, были проблемы?

Answer 1

В моем практическом опыте это выглядит так: «1. Логика первого порядка просто прекрасна». Примеры полных спецификаций для различных функций, полностью написанных на языке спецификаций, основанных на логике первого порядка, см., Например, ACSL по примеру или , это тематическое исследование .

Логика первого порядка имеет автоматические средства проверки (не помощники по проверке), которые были усовершенствованы в течение многих лет для обработки свойств скважины, полученных в результате проверки программы. Известными автоматизированными средствами проверки для этих целей являются, например, Упрощение , Z3 и Alt-ergo . Если эти средства проверки терпят неудачу и нет очевидной леммы / утверждения, которую вы можете добавить, чтобы помочь им, у вас все еще есть возможность запустить помощника по проверке для выполнения трудных обязательств по проверке. С другой стороны, если вы используете HOL, вы вообще не можете использовать Simplify, Z3 или Alt-ergo, и хотя я слышал об автоматических средствах проверки для логики высокого порядка, я никогда не слышал, чтобы их хвалили за их эффективность, когда дело доходит до свойств из программ.

Answer 2

Вы можете делать все, что вам нужно, в FOL, но это много дополнительной работы - много!Большинство существующих систем были разработаны академиками / людьми, у которых не так много времени, поэтому они склонны выбирать короткие пути, чтобы сэкономить время и усилия, и поэтому их привлекают HOL, функциональные языки и т. Д. Однако, если вы хотите создатьСистема, которая должна использоваться сотнями тысяч людей, а не просто сотнями, мы считаем, что FOL - это путь, потому что он гораздо более доступен для широкой аудитории.Там просто нет замены для выполнения работы;мы занимаемся этим уже 25 лет!Пожалуйста, взгляните на наш проект (http://www.manmademinions.com)

С уважением, Аарон.

Answer 3

Мы обнаружили, что FOL подходит для большинства условий проверки, но логика более высокого порядка неоценима для небольшого числа, например, для доказательства свойств суммирования элементов в коллекции. Таким образом, наш доказатель теорем (используемый в Perfect Developer и Escher C Verifier) ​​в основном первого порядка, но также способен выполнять рассуждения более высокого порядка.