II. Эталоны и методы проверки корректности.

Эталоны для проверки корректности программ могут использоваться в следующих трех формах, поясняемых с помощью рис.13:

1. Формализованные правила.

2. Программные спецификации.

3. Тесты.

Формализованные правила - имеют достаточно неопределенностей, так как опреде-ляются двумя видами требований

• требования стандартов (общероссийских и стандартов предприятий)

• требования языков и технологий программирования.

• синтаксический контроль

• семантический контроль

• структурный контроль.

• контроль полноты спецификаций

• верификация программ.

Статическое и динамическое тестирование

Рис.13

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

2. Программные спецификации - относятся к функциональным эталонам и в основ-ном обеспечивают проверку корректности программ в статике.

3. Тесты.

В зависимости от стадии и характера проверки разделяются тесты делятся на статические и динамические. Статическое тестирование - ручное тестирование программ, начиная со стадии формирования требований к программе. На стадии кодирования при статическом тестировании некоторую часть маршрутов исполнения тестируют вручную. Динамическое тестирование подразумевает достаточно полную структурную и функциональную проверку выполнения программы.

Как формируются эталоны для тестирования? Существует несколько способов формирования эталонов:

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

2. Использование моделирования на ЭВМ. Способ является универсальным. При этом ряд данных моделируется другим способом и по другим алгоритмам, нежели испытываемая программа и на других ЭВМ. Причем наборы входных данных создаются по случайным законам, что обеспечивает высокую гибкость этого способа.

3. Использование результатов испытаний предшествующих вариантов программ.

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

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

В 1-ом случае обеспечивается 100% гарантия корректности программ, в третьем случае такой уверенности нет, но мы можем убедиться в том, что программа работает так же или иначе, чем аналогичный вариант. Менее достоверные тесты приходится использовать из-за недостаточности сил и средств.

Лекция 9. Аналитическая проверка корректности программ. Верификация программ.

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

Различают два типа проверки корректности:

• валидация (validation) – установление соответствия между тем, что делает программа, и тем, что нужно Заказчику;

• верификация (verification) – установление соответствия между программой и ее спецификацией.

Определение верификациии симметрично ввиду относительного характера свойства корректности: если программа не соответствует своей спецификации, то либо программа, либо спецификация, либо оба этих объекта содержат ошибки. Перефразируя известное изречение Э.Дейкстры о тестировании программ, можно сказать, что верификация способна доказать отсутствие ошибок в программе, но не всегда доказывает их присутствие.

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

Можно сказать, что верификация – это вычисление истинности предиката от двух аргументов: программы и спецификации. Истинность этого предиката устанавливает свойство корректности программы, если спецификация не содержит ошибок, однако, его ложность, вообще говоря, не означает наличие ошибок в программе, а требует более точного разбора.

Учитывая специфику проявления ошибок в программах в процессе их выполнения на ЭВМ, целесообразно выделить в понятие корректности программы два свойства:

• частичную корректность – удовлетворение внешним (входной и выходной) спецификациям программы при условии завершения выполнения программы;

• завершенность – достижение в процессе выполнения выхода программы при определенных входной спецификацией данных.

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

Каждое из двух выделенных свойств корректности программы может удовлетворяться или не удовлетворяться. Таким образом, можно выделить шесть основных задач анализа корректности программы:

• частичная корректность (при условии завершенности);

• завершенность программы;

• незавершенность программы;

• тотальная корректность (частичная корректность и завершенность);

• частичная некорректность (некорректность при условии завершенности);

• некорректность (незавершенность или частичная некорректность).

Разделение свойств частичной корректности и завершенности следует рассматривать как методологический прием, направленный на уменьшение сложности верификации программ.

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

Введем ограничение: будем рассматривать программы, начинающиеся оператором 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 (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. Определение набора условий корректности для всех путей между соседними контрольными точками программы

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

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

U_: 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 – условный оператор _, тогда

U_i-1:   U_i при  = + или

U_i-1:   U_i при  = –

Пример

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

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) ) ) );

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

U_: P  ( g (f₁ (x) )  ( h ( f₂ (f₁ (x) ) )  Q ( f₃ ( f₂ (f₁ (x) ) ) );

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

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

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

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

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

Пример

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

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

r := x; q := 0;

while y  r do

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

Блок-схема этой программы имеет вид:

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

Разрежем цикл программы в точке входа в цикл (точка t₃)..

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

Запишем индуктивные утверждения для программы в контрольных точках t₁, t_ и t₃.

P: inv_t1( x, y )  ( x  0 )  ( y > 0 ); – условие корректных исходных данных

Q: inv_t2 ( x, y, q, r )  ( x = r + y*q )  ( r < y ); – условие выхода из цикла

inv_t3 ( x, y, q, r ) : x = r + y*q – инвариант цикла.

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

Путями между контрольными точками являются:

₁ : от входа программы к началу цикла (t₁ – t₃);

₂ : от начала цикла через тело цикла обратно к началу цикла (t₃ – t₃);

₃ : от начала цикла через условие цикла к выходу программы (t₃ – t₂).

Тогда

U_1 : P  inv_t3 ( r x, q  0 ) 

( x  0 )  ( y > 0 )  x = x + y*0 

( x  0 )  ( y > 0 )  x = x 

( x  0 )  ( y > 0 )  true

U_2 : inv_t3 ( x, y, q, r ) 

( ( y  r )  inv_t3 ( x, y, q  q+1, r r – y) ) 

(x = r + y*q )  ( ( y  r )  ( x = ( r - y ) + y*(q + 1)))  (x = r + y*q )  ( ( y  r )  (x = r + y*q ) );

U_3 : inv_t3 ( x, y, q, r )  ( ( y > r )  Q ) 

(x = r + y * q )  ( ( y > r )  (x = r + y * q )  ( r < y ) )

4. Доказательство истинности условий U_.

Условие U_1 – истина, так как x₁  x₂ – тождественная истина, если x₂ – истина.

Преобразуем условие U_2.

(x = r + y * q )  ( ( y  r )  (x = r + y * q ) ) 

( (x = r + y * q )  ( y  r ) )  (x = r + y * q ) ) 

( (x = r + y * q )  ( y  r ) )  ( x = r + y * q ) 

( x = r + y * q )  ( y  r )  ( x = r + y * q ) 

( y  r )  true  ( y  r )  true.

Следовательно, U_2 – истина (по аналогии с U_1).

Преобразуем условие U_3.

(x = r + y * q )  ( ( y > r )  (x = r + y * q )  ( r < y ) ) 

(x = r + y * q )  ( y > r )  (x = r + y * q )  ( r < y ) 

( y > r )  ( r < y ), так как x = r + y * q – true.

Следовательно, U_3 – истина

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

Пример 2

Доказать частичную корректность программы вычисленияz = [x] для любого целого x  0. [x] есть наибольшее целое число k такое, что k  x.

Решение

Метод вычисления, на котором основана программа, основывается на известном соотношении: 1 + 3 + 5 + … + (2k + 1) = (k + 1)² для каждого k  0.

Пусть значение суммы запоминается в s, а нечетные числа 2k + 1 – в n.

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

k := 0; s:= 0; n:= 1;

s := s + n;

while x  s do

begin k := k +1; n := n + 2;

s := s + n;

end;

z := k;

Блок-схема этой программы имеет вид:

1. Разрежем цикл программы в точке B.

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

Запишем индуктивные утверждения для программы в контрольных точках A, B и C.

P: inv_A(x)  x0 ; – условие корректных входных данных

Q: inv_С ( x, z )  (z²  x)  ( x < (z+1)² ); – условие выхода из цикла

inv_B (x, k, s, n): ( k²x )  ( s= (k+1)² )  ( n=2k+1 ) – инвариант цикла.

Определение набора условий корректности для всех путей между

соседними контрольными точками программы.

Путями между контрольными точками являются:

₁ : от входа программы к точке разреза цикла (A – B);

₂ : от точки разреза цикла через тело цикла обратно в точку разреза цикла (В – B);

₃ : от точки разреза цикла через условие цикла к выходу программы

( B – C).

Тогда

U_1 : P  inv_B (x, k, s s+n, n) 

( x  0 )  (k²  x )  ( s+n = (k+1)² )  ( n=2k+1 ) ) 

( x  0 )  ( 0²  x )  (0+1 = (0+1)²)  ( 1=2*0+1 ) ) 

( x  0 )  ( ( 0²  x )  (1 = 1)  (1 = 1) );

U_2 : inv_B (x, k, s, n)  ((sx) 

inv_B(x, k  k+1, s  s+n, n n+2)) 

( k²  x )  ( s = (k+1)² )  ( n=2k+1 )  ((s x) 

( (k+1)²  x )  ( s + n +2 = (k+2)² )  ( (n+2) = 2*( k+1) +1) );

U_3 : inv_B (x, k, s, n)  ( ( s  x )  inv_С ( x, z  k) ) 

( k²  x )  ( s = (k+1)² )  ( n=2k+1 )  ( ( s > x ) 

(k²  x)  ( x < (k+1)² )

Доказательство истинности условий U_.

Истинность всех трех условий легко проверяется подстановкой.

4.1. Условие U_1 – истина, так как

выражение ( x  0 )  ( ( 0²  x )  (1 = 1)  (1 = 1) ) 

(x  0)  (0  x)  (x  0)  (0  x)  (x < 0)  (x  0)  true

4.2. Преобразуем условие U_2.

( k²  x )  ( s = (k+1)² )  ( n=2k+1 )  ( (s  x) 

( (k+1)²  x )  ( s + n +2 = (k+2)² )  ( (n+2) = 2( k+1) +1) ) 

( ( k²  x )  ( s = (k+1)² )  ( n=2k+1 )  (s  x) ) 

( (k+1)²  x )  ( s + n +2 = (k+2)² )  ( (n+2) = 2( k+1) +1) )

Для доказательства истинности условия U_2 нужно показать, что соотношения, образующие конъюктивные члены справа от знака импликации, следуют из соотношений, стоящих слева от знака импликации.

а) Поскольку x  s и s = (k+1)², то (k+1)²  x.

б) s+n+2 = (k+1)² + 2k + 1 + 2  k² + 2k+ 1+ 2k + 1 + 2 = (k+2)²

в) n+2 = 2 (k+1) +2 = 2 (k+1)+1

Следовательно, условие истинно.

4.3. Преобразуем условие U_3.

( k²  x )  ( s = (k+1)² )  ( n=2k+1 )  ( ( s > x ) 

(k²  x)  ( x < (k+1)² ) 

( k²  x )  ( s = (k+1)² )  ( n=2k+1 )  ( s > x ) 

(k²  x)  ( x < (k+1)² )

Поскольку s > x и s = (k+1)², то (k+1)² > x и U_3 – истина

Анализ завершенности последовательных программ

Особенность свойства завершенности программ состоит в том, что оно не зависит от постусловия программы, и для заданной программы полностью определяется предусловием. В общем случае формальный анализ свойства завершенности представляет весьма сложную проблему.

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

• обращение к частично определенной функции со значением аргументов вне области определения;

• зацикливание.

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

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

Наибольшее распространение получили два метода логического анализа завершения циклических вычислений:

• метод Флойда;

• метод счетчиков.

Метод Флойда

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

Для формализации этой идеи в достаточно общей форме введем понятие фундированного множества.

Пусть S – частично упорядоченное множество относительно бинарного отношения  на его элементах, т.е. на множестве S для a, b и с  S выполняются свойства:

• антирефлексивности (a  a) ;

• антисимметрии a # b  ((b  a)) ;

• транзитивности a  b  b # c  a # c.

Множество S называется фундированным, если не существует бесконечной убывающей последовательности элементов из S.

Примеры фундированных множеств:

• множество натуральных чисел с отношением < ;

• множество ^* всех слов в алфавите , включая пустое слово с отношением w₁ < w₂, означающим что w₁ есть собственное подслово w₂.

Пусть Prgm – аннотированная программа, для которой методом индуктивных утверждений доказана частичная корректность. С каждой контрольной точкой r, лежащей на циклическом пути ( для этой точки существует обратный путь в точку r), свяжем частичную (ограничивающую) функцию _r (x₁, … , x_n), принимающую значения в фундированном множестве S.

Для каждого пути  между парой соседних контрольных точек r и t (r может совпадать с t), лежащих на циклическом пути, определим условие завершения в виде

W_: ( inv_r(x₁, …, x_n)  (_Û(x₁, …, x_n))  (_r(x₁, …, x_n)S 

_t(_(x₁, …, x_n))S  _r(x₁, …, x_n) _t(_(x₁, …, x_n))))),

где U_: inv_r(x₁, …, x_n)  (_Û(x₁, …, x_n))  inv_t(_(x₁, …, x_n)) – условие корректности метода индуктивных утверждений, _ – обратное преобразование, осуществляемое на пути  в методе индуктивных утверждений, т.е.

U₀ = _Û(x₁, …, x_n)  inv_t(_(x₁, …, x_n)), где (_r – ограничивающая функция вида X₁ X₂ … Xn  S, приписанная точке r.

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

Метод счетчиков

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

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

В отличие от метода Флойда этот метод не требует введения ограничивающих функций в контрольных точках. Переменные-счетчики рассматриваются как органическая часть программы, позволяющая логически выразить свойство завершенности в инвариантах цикла.

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

Успех доказательства завершенности в методе счетчиков определяется тем, удастся ли подобрать соответствующее условие ограниченности счетчика в инварианте цикла.

Этот метод, так же как и метод Флойда, требует творческого подхода программиста.