0
Каково применение символического выполнения? Do symbolic execution генерировать только path condition? Как использовать символическое выполнение для проверки contract?применение символического исполнения
A
ответ
1
Наиболее известным использованием символического исполнения является создание тестового ввода. Например, KLEE - это инструмент, который генерирует тестовые входы для программ C, используя символическое выполнение.
Другое приложение будет проверять утверждение. Если по контракту вы имеете в виду условия до и после, то да, символическое исполнение также может быть использовано для этой цели.
большое спасибо. Выполняет ли символическое выполнение тестовый ввод только с помощью помощника по решению ограничений? Не могли бы вы рассказать мне больше о том, как использовать символическое исполнение для проверки условий до и после? – any
Насколько я знаю да, он генерирует тестовые входы с помощью решателя ограничений. Простейшая идея: представьте, что у вас есть функция с условиями до и после. Используя символическое выполнение, вы найдете условие пути для всех возможных путей этой функции. Если «пост-условие и условие пути» выполняется во всех путях, то выполняется условие post. – afsafzal
Спасибо за вашу любезную помощь. если «пост-условие и условие пути» является выполнимым или «предварительное условие и условие пути»? – any