ВОЗМОЖНОСТИ ИСПОЛЬЗОВАНИЯ ФУНКЦИОНАЛЬНЫХ ЯЗЫКОВ ДЛЯ АВТОМАТИЗАЦИИ ЗАДАЧ ВЕРИФИКАЦИИ

Соколов Илья Николаевич

Интерпретируемые языки программирования с динамической типизацией позволяют достаточно быстро писать программы и даже комплексы программ. Однако проблемные вопросы спецификации и верификации программ, написанных на таких языках практически, не поддаются автоматизации и зачастую выполняются вручную. В данной статье предложен метод автоматизированной верификации программ написанных на языках с динамической типизаций. Для решения вопросов с типами программа транслируется в функциональный язык программирования который используется в качестве языка спецификации с последующей параметризацией аргументов и построением полноценной модели для property-based тестирования.

Ключевые слова:Верификация программ, тестирование, функциональные языки программирования, спецификация, формальные методы, property-based testing