Автоматизация верификации программ

Содержание

 

Основные задачи анализа корректности программ ……..………………......	.… 2
Метод индуктивных утверждений ……………………………….….……....	…. 7
Анализ завершения последовательных программ ……………...….………..	. 13
Основные концепции формализации семантики программ, аксиоматическая система Хоара ……………………………………………...	. 16
Автоматическая генерация и доказательство условий корректности .….…	. 21
Специфика верификации недетерминированных и параллельных программ ……………………………………………………………………….	.. 24
Литература …………………………………...…………………………..…….	. 27

 

 

Основные задачи анализа корректности программ

 

Рассмотрим формальные постановки задач анализа корректности.

Введем ограничение: будем рассматривать программы, начинающиеся оператором START (первый выполняемый оператор) и заканчивающиеся оператором STOP (последний выполняемый оператор).

Спецификацию программы Prgm будем определять путем приписывания индуктивных утверждений точкам разреза графа потоков управления программы (точкам между операторами программы). При этом выходу оператора START приписывается входной предикат (предусловие) программы P(x), определяющий множество допустимых значений исходных данных  x (x допустимо, если P(x): true), а входу оператора STOP приписывается выходной предикат (постусловие) Q(x,y), определяющий целевую функцию программы (связь между входными и выходными данными программы).

Тогда свойство частичной корректности программы определяется следующей формулой логики предикатов:

PCOR(Prgm, P, Q):  "x ( P(x) Ù fin(x) Þ Q( x, f(x) ) ),

где fin(x) – предикат завершения программы Prgm, начатой в состоянии x;

f(x) – функция, вычисляемая программой Prgm,

свойство завершенности может быть определено формулой:

FIN(Prgm, P): "x ( P(x) Þ fin(x) ),

а свойство тотальной корректности формально выражается как одновременное присутствие свойств частичной корректности и завершенности:

TCOR(Prgm, P, Q): "x ( P(x) Þ Q(x, f(x) ) Ù fin(x) ).

Аналогичным образом могут быть формализованы и другие перечисленные  выше свойства корректности (записать самостоятельно).

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

Наиболее распространенным методом  доказательства частичной корректности программ является метод индуктивных утверждений, предложенный Флойдом. Он позволяет свести доказательство частичной корректности программы к доказательству некоторого конечного числа утверждений, записанных на языке исчислений предикатов первого порядка и имеющих интерпретацию в соответствующей проблемной области.

Рассмотрим метод индуктивных  утверждений для программ с конечным множеством простых переменных { x₁, x₂, … x_n }, где n³1, а операторами являются:

• операторы присваивания вида  x_i := f (x₁, x₂, … x_n);
• составной оператор вида A ; B ;
• оператор условного перехода if a(x₁, x₂, … x_n) then L₊ else L_– ,

где L₊, L_– – метки операторов, которым передается управление;

• начальный оператор START;
• конечный оператор STOP.

Такой состав структурных компонентов  вполне достаточен для представления  произвольного алгоритма и поэтому  не ограничивает общности излагаемого  метода.

Установление частичной корректности осуществляется за четыре последовательных шага.

Шаг 1. Разрезание циклов программы

Очевидно, что при выполнении программы  для различных исходных данных возможны различные последовательности операторов, начинающиеся оператором START и оканчивающиеся оператором STOP. Назовем такие последовательности трассами вычислений.

Сложность анализа частичной корректности программы разбиением на трассы заключается в том, что при наличии циклов в программе он не может быть выполнен непосредственным перебором всех трасс. Эта сложность может быть преодолена путем включения в граф потока управления программы конечного числа точек, называемых точками разреза, таким образом, что каждый цикл содержит одну такую точку, которая “разрезает” циклические пути на два:

• путь через тело цикла;
• путь к выходу из цикла.

Шаг 2. Получение  аннотированной программы

С каждой точкой разреза k свяжем предикат

inv_k (x₁, … , x_n),

который будем называть индуктивным утверждением. Назначение этого предиката состоит в том, чтобы описать соотношение между переменными в этой точке. Всякий раз, когда исполнение программы достигает точки k, предикат   inv_k (x₁, … , x_n) должен  быть истинным  для  текущих  значений x₁, … , x_n в этой точке.

Индуктивное утверждение, приписанное  циклу, принято называть инвариантом цикла. Инвариант цикла может приписываться точке входа в цикл или любой другой точке цикла, которая лежит на каждой трассе через цикл.

Будем считать, что программа аннотируется выбором контрольных точек (на входе программы, выходе программы и на каждом пути через цикл), с каждой из которых связывается индуктивное утверждение (инвариант):

inv_t1 (x₁, … , x_n): P ;   inv_t2 (x₁, … , x_n): Q ;   inv_t3 (x₁, … , x_n) ; … ,

где t1 – точка входа (после оператора START), t2 – точка выхода (перед оператором STOP), t3 – контрольная точка инварианта цикла.

Шаг 3. Определение  набора условий корректности для  всех путей между соседними контрольными точками программы

Пусть путь a ведет от контрольной точки r  к контрольной точке t (случай  r = t не исключается) и не содержит никаких других контрольных точек и пусть этот путь проходит через последовательность операторов A₁, A₂, … , A_i,, … , A_k, где A_i – оператор присваивания или условие r_e,  где e Î { +,  - }.

Определим условие U_a пути a между двумя соседними контрольными точками графа потока управления программы следующим образом:

U_a: inv_r(x₁, … , x_n) Þ U₀

(из истинности предиката в  начальной контрольной точке r следует истинность условия U₀), где последовательность U₀, U₁, … , U_k задается по индукции (методом обратной подстановки):

1. U_k: inv_t (x₁, … , x_n) – условие определяется предикатом в контрольной точке t;
2. Пусть U_i определено. Тогда возможны два случая:

1. A_i – оператор присваивания x_s := f (x₁, … , x_n), тогда

     U_i-1:  U_i ( x_s ¬ f (x₁, … , x_n));

2. A_i – условный оператор r_e, тогда

    U_i-1:  r Þ U_i  при e = + ,  или

    U_i-1:  Ør Þ U_i  при e = –

Пример

Пусть a соответствует последовательности:

x = f₁ (x);   g₊ (x);   x = f₂ (x);   h_– (x);      x = f₃ (x);

Тогда  P :  inv_r (x)  – входной предикат;

U₅ : Q = inv_t (x);

U₄ :  Q ( f₃ (x) );

U₃ :  ( Ø h (x)  Þ Q ( f₃ (x) ) );

U₂ :  ( Ø h ( f₂ (x) ) Þ Q ( f₃ ( f₂ (x) ) ) );

U₁:  ( g (x)  Þ (Ø h ( f₂ (x) ) Þ Q ( f₃ ( f₂ (x) ) ) );

U₀:  ( g (f₁ (x) )  Þ (Ø h ( f₂ (f₁ (x) ) ) Þ Q ( f₃ ( f₂ (f₁ (x) ) ) );

Окончательно условие пути a имеет вид:

U_a:  P Þ (  g (f₁ (x) )  Þ (Ø h ( f₂ (f₁ (x) ) ) Þ Q ( f₃ ( f₂ (f₁ (x) ) )  );

Шаг 4. Доказательство истинности составленных условий корректности

Введенное понятие условия U_a между соседними контрольными точками позволяет свести задачу анализа частичной корректности программы Prgm к доказательству истинности условий между любыми соседними контрольными точками программы Prgm.

Теорема (без док-ва). Программа Prgm частично корректна относительно предусловия  P и постусловия Q, если для каждого пути a между соседними контрольными точками условие пути U_a истинно.

Важность этой теоремы состоит  в том, что она позволяет абстрагироваться от конкретных процессов между соседними  контрольными точками вычислений по программе и рассматривать только условия U_a между соседними контрольными точками, т.е. рассматривать только характеристики статической структуры программы.

Возможности доказательства условий  корректности U_a зависят от проблемной области.

Пример

Доказать частичную корректность программы вычисления частного и остатка от деления целых чисел x и y.

Программа на Паскале:

r := x;   q := 0;

while  y £ r  do

begin   r := r – y;    q := q + 1 end

 

Метод индуктивных  утверждений

 

Метод индуктивных  утверждений независимо сформулирован  К. Флойдом и П. Науром.

Суть этого метода состоит  в следующем:

1) формулируются входное  и выходное утверждения: входное  утверждение описывает все необходимые  входные условия для программы  (или программного фрагмента), выходное  утверждение описывает ожидаемый результат;

2) предполагая истинным  входное утверждение, строится выведенное утверждение, которое выводится на основании семантики операторов, расположенных между входом и выходом (входным и выходным утверждениями);

3) формулируется теорема  (условия верификации): из выведенного утверждения следует выходное утверждение;

4) доказывается теорема,  что свидетельствует о правильности  программы (программного фрагмента).

Пусть А – утверждение, описывающее предполагаемые свойства данных в программе, а С - утверждение, описывающее то, что по предположению требуется получить в результате выполнения программы (утверждение о правильности). Программа частично правильна, если при каждом ее выполнении с данными, удовлетворяющими предположению А, будет справедливо утверждение С при условии, что программа закончится.

Программа полностью правильна, если она частично правильна и заканчивается при всех данных удовлетворяющих предположению А.

Представлен метод следующем  образом:

Пусть P блок-схема, а a – путь в этой блок-схеме, начинающийся со связки e₀ и завершающийся связкой e_k:

n₀ –e₀® n₁ –e₁® … n_k –e_k® n_k+1

Дадим несколько вспомогательных  определений. Определим предикат допустимости R_a(x,y) : D_x ´ D_y ® { Т, F } и функцию пути r_a(x,y) : D_x ´ D_y ® D_y. Предикат допустимости R_a(x,y) определяет, какое должно быть значение входных и промежуточных переменных в начале пути, чтобы дальнейшее вычисление шло по пути a. Функция пути r_a(x,y) определяет, как изменятся значения промежуточных переменных в результате исполнения всех операторов блок-схемы лежащих на пути a.

Наиболее простым способом вычисления предиката допустимости R_a(x,y) и функции пути r_a(x,y) является метод обратных подстановок.

Пусть последовательность операторов внутри пути a есть n₁, …, n_k. Для каждого m Î { 1, …, k+1 }, определим предикат R_a^m(x,y) и функцию r_a ^m(x,y). При этом для m £ k, функция r_a(x,y)  будет являться функцией пути, проходящего через операторы n_m, …, n_k, а предикат R_a^m(x,y) будет являться предикатом допустимости для этого же пути.

Таким образом,

R_a(x,y) º R_a¹(x,y)

r_a(x,y) º r_a¹(x,y)

Предикаты R_a^m(x,y) и функции r_a(x,y) мы определим индукцией по m.

Базис индукции:

R_a^k+1( x, y ) º T

r_a^k+1( x, y ) º y

Индуктивное предположение:

Предположим, что R_a^m+1(x,y) и r_a^m+1(x,y)  уже определены для некоторого m Î { 2, …, k+1 }.

Индуктивный переход:

Определим в зависимости R_a^m(x,y) и r_a^m(x,y) от оператора n_m:

• Если n_m – оператор присваивания ASSIGNMENT: y ¬ g( x, y ), то

R_a^m( x, y ) º R_a^m+1( x, g( x, y ) )

r_a^m( x, y ) º r_a^m+1( x, g( x, y ) )

• Если n_m – условный оператор TEST: t( x, y ) и связка e_m помечена символом T, то

R_a^m( x, y ) º R_a^m+1( x, y )

r_a^m( x, y ) º r_a^m+1( x, y ) ∧ t( x, y )

• Если n_m – условный оператор TEST: t( x, y ) и связка e_m помечена символом F, то

R_a^m( x, y ) º R_a^m+1( x, y )

r_a^m( x, y ) º r_a^m+1( x, y ) ∧ Øt( x, y )

• Если n_m – оператор соединения JOIN, то

R_a^m( x, y ) º R_a^m+1( x, y )

r_a^m( x, y ) º r_a^m+1( x, y )

Заметим, что операторы других типов (начальный и завершающий) не могут  встречаться на пути, так как они  не имеют либо входящих, либо выходящих  связок.