| 0 |
|
Группа программных инженеров из Мичиганского университета, Microsoft Research и Университета Карнеги-Меллона (штат Пенсильвания) представила созданную ими систему Armada, для проверки правильности работы сложных программ без необходимости тестировать их с полным диапазоном возможных входных величин.
«По сути, если вы не перепробуете все возможные входные данные, то можете что-то упустить, — говорит профессор Манос Каприцос (Manos Kapritsos), соавтор статьи, представленной на конференции Programming Language Design and Implementation (PDLI 2020). — И на практике это происходит сплошь и рядом. Системы, о которых мы говорим, очень сложны, и тестировщики не могут исчерпывающе проверить все варианты их поведения».
Армада использует альтернативный метод, так называемой формальной верификации. Она подходит к задаче с позиций математической логики, строя доказательство того, что ошибки в данной программе невозможны.
Формальная верификация не всегда является панацеей. Поиск удовлетворительного доказательства сложных, в том числе конкурентных или многопотоковых программ, часто превращается в длительный и ресурсоемкий процесс.
Armada подвергает подобный сложный код серии преобразований, разбивая его на более простые фрагменты. Разработчикам остаётся доказать, что каждый упрощенный код действительно является представлением более сложной программы с предыдущего этапа.
Для этого разработчик с помощью высокоуровневого синтаксиса Armada составляет краткое описание своего программного обеспечения и используемых методов проверки, на основе чего система автоматически генерирует значительно более длинное полное доказательство. В одном из случаев такое итоговое доказательство содержало 24 540 строк, при этом вручную было написано только 70 строк этого кода.
В случае неудачи доказательства пользователь генерирует новое: с изменённым описанием или другим методом из библиотеки Armada. Система использует верификатор для проверки надёжности всех предлагаемых ею методов доказательства, и допускает расширение их ассортимента в дальнейшем.
В конце концов, разработчик получает простую высокоуровневую спецификацию всей своей программы, затратив рекордно малые усилия на верификацию сложного многопотокового кода.
Авторы надеются, что эта сокращённая и упрощённая процедура будет способствовать самому широкому применению формальной верификации, а не только в самых ответственных системах, где она уже используется за неимением разумной альтернативы.
Ready, set, buy! Посібник для початківців - як придбати Copilot для Microsoft 365
| 0 |
|
