Метод символического выполнения (м.Кинг, ibm, 1967)

Цель: генерация структурных тестов. Идея метода: установить соответствие между классами вх (и заодно, вых) данных и возможными путями в программе, прослеживая условия прохождения того или иного пути. Идею иллюстрирует рис. 11-1, где классы эквивалентности представлены связными точечными областями, а стрелкам соответ-ствуют различные пути - траектории вычислений, приводящие к отображению вх данных на вых. Звездочками отмечены точки – тестовые данные. Идея в том, чтобы вместо реального выполнения программы на тестовых данных проводить «символическое» выполнение сразу на классе вх данных.

Рис. 11-1. Программа как функциональный преобразователь.

Классы вх, вых и промежуточных данных описываются условиями, т.е. предикатами на множестве данных. Операторы программы «преобразуют» предикаты, например:

k > 0 B

k = k + 6

да нет

a > 2

k > 2

k > 6 В & a > 2 В & a =< 2

Проследив преобразования на протяжении всего конкретного пути, получим условие его прохождения в виде конъюнкции такого количества термов, сколько разветвлений на этом пути. Это – формальная операция и поэтому может быть автоматизирована. Эта импликация описывает класс исходных данных, эквивалентный данному пути. Однако чтобы найти явное выражение для входных данных, приходится разрешать это логическое выражение относительно искомых переменных. В численных алгоритмах это приводит к решению системы неравенств, в общем случае нелинейных. (Задание 1).

Их решение тоже можно автоматизировать, что и попытался сделать М.Кинг в системе EFFIGY для подмножества Кобола (1971). Сложность численных методов не позволила построить эффективную программу для практических нужд, однако идея программы, аннотированной условиями, нашла развитие в работах Флойда, Дейкстры и Хоара, посвященных формальной верификации.

Альтернатива тестированию: понятие формальной верификации программ

- т.е., доказательства правильности программ без их выполнения. Идея: доказывать программу логически, как теорему. Подход Дейкстры – Хоара: метод наислабейшего предусловия – применение логики предикатов первого порядка для описания свойств и поведения программ. Состояние программы = состояние памяти = отображение множества идентификаторов на множество значений. Предикат P выражает множество состояний, в которых он истинен. И наоборот, для любого множества состояний можно построить предикат, его выражающий.

Y P (X,Y) = X>0 & X>Y

S

P 0 X

Q

P { S }Q – тройка Хоара:

S - программа или фрагмент программы;

P - предусловие – предикат, характеризующий множество начальных состояний;

Q - постусловие – предикат, характеризующий множество конечных состояний.

Если S – программа, то P и Q задают логическую спецификацию программы.

Примеры:

1. Вычислить приближенное значение R - корня квадратного из N

(R округляется до целого): { N >= 0 } S { R² =< N < (R + 1)² }

2. Упорядочить по возрастанию числовой массив из n элементов:

{ N > 0 } S { i : 0  i  n-2: b[i]  b[i + 1] }

(Задание 2)

Цель верификации – доказать, что если до выполнения программы истинно P, то программа завершается в состоянии истинности Q. Идея Хоара: описать семантику каждого оператора языка программирования формально и использовать эти утверждения для доказательства программы. Семантика описывается т.н. наислабейшим предусловием wp (weakest predicate). Это – функция программы (фрагмента программы, оператора) S и постусловия R. Функция wp (S, R) описывает множество всех состояний, для которых выполнение S обязательно закончится через конечное время в состоянии, удовлетворяющем R.

Например, wp ( ‘i:= i + 1; i  1 ) = ( i  0 ) . Заметим, что ( i < - 5 ) – тоже предикат, истинный для S, R, но более сильный, чем ( i  0 ).

Q { S } R – другая форма записи предиката Q  wp ( S, R ), где  - знак импликации. wp как функция обладает определенными свойствами, например:

• wp (S, Q) & wp (S, R) = wp (S, Q & R) – дистрибутивность конъюнкции

• Если Q  R, то wp (S, Q)  wp (S, R) – закон монотонности

Эти и другие свойства используются при формальной верификации.

Аксиоматическое задание семантики операторов

1. Последовательность операторов S1; S2

wp ( 'S1; S2', R ) = wp (S1, wp ( S2, R )), поскольку wp ( S2, R ) - это постусловие для S1.

2. Оператор присваивания: wp ( 'x:= e', R ) = R _{x e}

(т.е., в предикате R все вхождения x заменены на e).

Например, wp ( ‘x = 2 * y + 3 ‘, x = 13 ) = ( 2*y + 3 = 13) = (y = 5)

3. Оператор выбора IF (аналог оператора case):

if B₁  S1 где: B_i – предохранители - предикаты