Аспекты автоматической генерации верификационных наборов тестовых процедур. Разработка алгоритма нахождения тестовых наборов посредством трансляции программ в логические выражения и их преобразования для решения задачи выполнимости булевых формул.
Аннотация к работе
Обычно тесты представляют собой набор "входных" параметров, подающихся на вход в программу, а по завершении ее работы "выходные" параметры сравниваются с "ожидаемыми" по логике, описанной в спецификации. Задача о выполнимости булевых формул (the Boolean Satisfiability Problem или SAT) - задача, которая заключается в определении: существуют ли такие значения переменных, при которых данная булева формул (набор переменных, скобок и операций конъюнкции, дизъюнкции и логического отрицания) получает значение "истина". SAT-решатели фокусируются на задаче в конъюнктивной нормальной форме, так как для формул в дизъюнктивной нормальной форме решение тривиально и производится за линейное время - для разрешимости достаточно, чтобы присутствовала хотя бы одна конъюнкция, не содержащая одновременно противоположные литералы. Обычно решение SAT задачи заключается лишь в ответе на вопрос "существует ли такой набор значений переменных, при котором формула обращается в 1". Необходимо учесть, что задачи для CNF-SAT-решателей принято формулировать следующим образом: первая строка текстового документа должна отображать информацию о "проблеме" (через пробел вводится количество переменных и количество дизъюнктов); каждая следующая строка представляет собой дизъюнкт, переменные в котором также разделяются пробелом; каждый дизъюнкт завершается нулем "0"; в качестве переменных выступают числа, соответствующие индексу переменной; если перед переменной стоит знак "-", то это обозначает отрицание данной переменной.