ЗАСТОСУВАННЯ СОЛВЕРІВ Z3 В СИСТЕМІ ВЕРИФІКАЦІЇ PYTHON–ПРОГРАМ
DOI:
https://doi.org/10.32689/maup.it.2023.1.5Ключові слова:
верифікація програми; умова коректності; символьне виконання; контрприклад; солвер Z3Анотація
У роботі описана остання версія системи верифікації програм VerPro на мові Python. Для перевірки тотожної істинності умов верифікації вона доповнена застосуванням засобів популярної системи Z3 доведення теорем. Метою статті є опис нових можливостей системи VerPro, які їй надали солвери Z3. Наукова новизна. Система VerPro є сучасною системою верифікації анотованих Python–програм, яка генерує умови коректності методом символьного виконання. VerPro надає користувачу сучасний діалоговий графічний віконний інтерфейс, побудований з використанням бібліотеки PyQt5. Спрощення цих умов базується на еквівалентних перетвореннях, які реалізує бібліотека ExprLib. ExprLib – це наша власна бібліотека, яка побудована на мові Python і не має інших залежностей. Бібліотека перетворює вирази у внутрішнє представлення, побудоване на базі класів мови Python. Реалізовані в системі VerPro еквівалентні перетворення часто можуть самі встановити тотожну істинність умов верифікації. Якщо ні, тоді такі умови VerPro передає системі доведення теорем Z3, яка або встановлює їх тотожню істинність, або будує контрприклад для гіпотези про тотожню істинність такої умови. Наявність контрприкладу свідчить про те, що анотація невірно описує функціональні властивості програми. Аналізуючи знайдений системою контрприклад, користувач може знайти причину некоректності і виправити програму і/або її анотацію. Система Z3 підключається до VerPro через програмний інтерфейс Z3py. Висновок. Ідея побудови контрприкладів в системах верифікації програм реалізована вперше. Cистема доведення теорем Z3 раніше в таких системах не застосовувалася. Система VerPro надає приклад вдалого використання сучасної системи доведення теорем не лише для встановлення коректності анотованої програми, але й для пошуку рішення при невдалій верифікації. Дальший розвиток системи передбачає типізацію значень символьних параметрів та побудову інваріантів.
Посилання
Костирко В.С. Система верифікації python–програм. Матеріали ХXV Міжнародної науково-практичній конференції. К.: Європейський університет. 2019. С. 75–78.
Floyd, R. W. Assigning meanings to programs. Proceedings of a Symposium on Applied Mathematics. American Mathematical Society. 19 Mathematical Aspects of Computer Science. 1967. 19–31.
Z3 API in Python. Retrieved from: https://ericpony.github.io/z3py-tutorial/guide-examples.htm.
Костирко, В. С., Плеша, В. І. (2021). Система верифікації програм VerPro. Сучасні напрями розвитку економіки, підприємництва, технологій та їх правового забезпечення: матеріали Міжнародної науково-практичної конференції. Львів: Львівський торговельно-економічний університет. 287–288.
PyQt5 Reference Guide. Retrieved from: https://www.riverbankcomputing.com/ static/Docs/PyQt5/.
Костирко, В.С., Плеша, В. І. Застосування бібліотеки Z3py для перевірки умов коректності та завершимості програм. Матеріали ХXVІ міжнародної науково-практичної інтернет–конференції. К.: Європейський університет. 2020. 80–83.
Wayne, H. Retrieved from: https://github.com/hwayne/lets-prove-leftpad.
Bruni, R., Giacobazzi, R., Gori, R., Ranzato, F. (2023). A Correctness and Incorrectness Program Logic. Journal of the ACM. 70. 1–45. DOI: https://doi.org/10.1145/3582267.
Stump, A. (2016). Verified Functional Programming in Agda. Association for Computing Machinery and Morgan & Claypool. DOI: https://doi.org/10.1145/2841316.
Vardi, M. Y. (2021). Program verification: vision and reality. Communications of the ACM (CACM). 64 (7). 5. DOI: https://doi.org/10.1145/3469113.
