ПРОЄКТУВАННЯ БІБЛІОТЕКИ ДЛЯ СПРОЩЕННЯ УМОВ ВЕРИФІКАЦІЇ ПРОГРАМ
DESIGNING A LIBRARY TO SIMPLIFY PROGRAM VERIFICATION CONDITIONS
Сторінки: 273-279. Номер: №3, 2023 (321) 
Автори:
КОСТИРКО ВАсиль
Львівський торговельно-економічний університет
ORCID ID: 0000-0002-6366-8695
e-mail: vkostyrko@lute.lviv.ua
АНІЛОВСЬКА Ганна
Львівський торговельно-економічний університет
ORCID ID: 0000-0002-0154-1584
e-mail: hjaa5514@gmail.com
ПЛЕША Василь
Львівський торговельно-економічний університет
ORCID ID: 0000-0001-5321-9602
e-mail: plesha_v@i.ua
KOSTYRKO VASYL, ANILOVSKA HANNA, PLESHA VASYL
Lviv University of Trade and Economics
DOI: https://www.doi.org/10.31891/2307-5732-2023-321-3-273-279
Анотація мовою оригіналу
Анотація програми інваріантами, заданими в певних точках програми, зводить проблему її верифікації до перевірки істинності ряду логічних виразів. Однак, проблема виводимості є алгоритмічно нерозв’язною навіть для достатньо простих предметних областей, таких як елементарна арифметика. Тому важлива розробка комп’ютерних засобів, які можуть спростити задачу верифікації програм. Особливо важлива наявність таких систем для навчання програмуванню. До них відносяться технологія символьного виконання програм та інструменти для еквівалентних перетворень та спрощення символьних виразів. Залишаються актуальними дослідження формальних методів верифікації програм. У статті описана побудована на базі бібліотеки ExprLib технологія автоматичного еквівалентного перетворення арифметичних та логічних виразів до найпростішого стандартизованого вигляду. Досліджено побудовані перетворення. Встановлено, що вони мають властивість ідемпотентності, а еквівалентні вирази мають єдине нормалізоване представлення. Бібліотека написана алгоритмічною мовою Python з використанням рекурсії на структурах даних типу дерево. Бібліотека реалізована класами та функціями мови Python, які представляють деревовидні структури списками, множинами та словниками мови Python. Побудовано класи для представлення дерев, одночленів та поліномів, відношень та їх кон’юнкцій, а також імплікацій. Для спрощення імплікацій застосовується правило редукції кон`юнкцій. Бібліотека застосовується в системі VerPro символьного виконання та верифікації програм на мові Python. Для перевірки тотожної істинності імплікацій, які представляють умови верифікації, використовуються солвери системи доведення теорем Z3. Система VerPro є експериментальною і зараз обмежується програмами цілочисельної арифметики. Наявність власної бібліотеки дозволяє розширювати область застосування системи, яка розвивається в напрямку генерації інваріантів та розширення областей охоплених нею програм.
Ключові слова: бібліотека функцій і класів; мова Python; еквівалентні перетворення виразів; умова коректності; дерево виразу; верифікація програм.
Розширена анотація англійською мовою
The ExpLib library described for the equivalent transformation of arithmetic and logical expressions in order to reduce them to the simplest form based on the classical relations of integer arithmetic and mathematical logic. Annotating the program with invariants specified at certain points of the program reduces the problem of program verification to checking the truth of a set of logical expressions. However, the problem of derivability is algorithmically unsolvable even for sufficiently simple subject area, such as elementary arithmetic. Therefore, it is important to develop computer tools that can simplify the task of program verification. It is especially important to have such systems for programming teaching. These include the technology of symbolic execution of programs and tools for equivalent transformation and simplification of symbolic expressions. Formal methods of program verification are reflected in many modern studies. The article describes the technology of automatic equivalent conversion the arithmetic and logical expressions to the simplest standardized form built on the basis of the ExprLib library. These transformations have the property of idempotency, and the equivalent expressions have a single normalized representation. The library is written in the Python algorithmic language using recursion on tree-type data structures. The library is implemented by classes and functions built in Python using lists, sets, and dictionaries. These classes represent trees, monomials and polynomials, relations and their conjunctions, as well as implications. To simplify the implications, the reduction rule of conjunctions is used. The ExpLib is used in the VerPro system for symbolic execution and Python programs verification. To verify the identical truth of the implications, which represent the verification conditions, solvers of the Z3 theorem proving system are used. The VerPro system is experimental and currently limited to integer arithmetic applications. Having the own library allows us to expand the scope of the system. The VerPro system is developing in the direction of invariant generating and expanding the program area.
Keywords: library of functions and classes; Python language; equivalent transformations of expressions; correctness condition; expression tree; program verification.
