Техника символьного выполнения
Техника логического доказательства игнорирует структуру и синтаксис ЯП, в которых тестовые программы выполняются. В случае, когда техника доказывает, что спроектированные компоненты являются правильными, они необязательно выполняются. Одна из таких техник – символьное выполнение – включает моделирование выполнения кода, используя символы вместо переменных данных. Тестовая программа рассматривается как имеющая детерминированное входное состояние при вводе данных и условий. Благодаря этому каждая строка кода выполняется, а данная техника проверяет, изменилось ли состояние. Каждое измененное состояние сохраняется, и выполняемая программа рассматривается как серия изменений состояний. Последнее состояние каждой части будет выходным состоянием и программа будет правильной.
Символьная проверка приводится на примере нескольких строк фрагмента программы:
а = b + с ;
if (a > d) task x ( ) ; // выполнить задание х
else task y ( ); // выполнить задание у
В нем проверяется условие a>d на истинность или нет. Поскольку выполнение условного кода включает значения переменных а и d, то рассматривается два случая, определенные на двух отдельных эквивалентных классах, когда условие верно и получен соответствующий результат. И второй случай, когда условие не выполняется.
Описание доказательства может оказаться длиннее написанного фрагмента программы и нет уверенности, что это описание не содержит ошибок. Данная стратегия имеет преимущество перед логическим доказательством теорем, поскольку полагается на трассирование изменяющихся условий операторов программв. Главными элементами доказательства корректности программы являются фрагмент программы, входные и выходные значения переменных, а также процесс слежение за тем, как этот фрагмент программа будет выполняться.