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

Для этих операторов, мы расширим определения  предиката допустимости и функции  пути. Если началом первой связки пути является начальный оператор START: y ¬ f( x ), то мы будем говорить, что предикат допустимости R'_a(x) º R_a( x, f( x ) ), а функция пути r'_a(x) º r_a(x, f( x ) ). Если концом последней связки пути является завершающий оператор HALT: z ¬ h( x, y ), то мы будем говорить, что функция пути r''_a( x, y ) º h( x, r_a( x, y ) ) ( r''_a( x, y ) : D_x ´ D_y ® D_z ).

Индуктивные утверждения.  Пусть P – блок-схема, а F = ( , y ) – ее спецификация. Рассмотрим следующий метод доказательства частичной корректности программы P относительно спецификации F.

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

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

Шаг 2. Индуктивные  утверждения.  Выберем для каждой точки сечения i предикат p_i(x, y), который характеризует отношение между переменными блок-схемы при прохождении данной связки. Часто, эти предикаты называют индуктивными утверждениями. Кроме того, свяжем входной предикат (x) с начальным оператором блок-схемы, а выходной предикат y(x, z) – со всеми завершающими операторами.

Шаг 3. Условия  верификации.  На третьем шаге, сконструируем для каждого промежуточного базового пути a, начинающегося в точке сечения i и завершающегося в точке сечения j, условия верификации:

" x Î D_x  " y Î D_y  [ p_i(x, y) ∧ R_a(x, y) Þ p_j( x, r_a(x, y) ) ]

Эти условия утверждают, что если предикат p_i(x, y) истинен для некоторых значений переменных x и y, и эти значения такие, что начиная из точки сечения i вычисление пойдет по пути a, то предикат p_j(x, y) будет истинен для значений переменных x и y, после прохождения по пути a.

Для начального базового пути a, завершающегося в точке сечения j, условия верификации будут выглядеть следующим образом:

" x Î D_x  [ (x) ∧ R'_a(x) Þ p_j( x, r'_a(x) ) ]

В этом случае, условия утверждают, что если входной предикат (x) истинен для некоторых значений входных переменных, и эти значения такие, что начальное вычисление пойдет по пути a, то предикат p_j(x, y) будет истинен для значений переменных x и y, после прохождения по пути a.

Для каждого конечного базового пути a, начинающегося в точке сечения i, условия верификации конструируются следующим образом:

" x Î D_x  " y Î D_y  [ p_i(x, y) ∧ R_a(x, y) Þ y( x, r''_a(x, y) ) ]

Здесь, условия верификации утверждают, что если предикат p_i(x, y) истинен для некоторых значений переменных x и y, и эти значения такие, что начиная из точки сечения i вычисление пойдет по пути a, то предикат y(x, z) будет истинен для значений переменных x и z, после завершения работы блок-схемы при прохождения по пути a.

Если в  блок-схеме существуют простые базовые  пути, то для каждого такого пути a условие верификации будут выглядеть следующим образом:

" x Î D_x  [ (x) ∧ R'_a(x) Þ y( x, r''_a( x, r'_a(x) ) ) ]

В этом случае, условия утверждают, что если входной предикат (x) истинен для некоторых значений входных переменных, и эти значения такие, что вычисление пойдет по пути a, то выходной предикат y(x, z) будет истинен для значений переменных x и z, после завершения работы блок-схемы при прохождения по пути a.

Лемма. Пусть все условия верификации истинны. Пусть дано вычисление блок-схемы P, входные переменные которого удовлетворяют входному предикату . Тогда для каждого прохода вычисления C_k – C_k+1 через точку сечения i, предикат p_i(x, y) будет истинен на значениях переменных x и y в конфигурации C_k.

Теорема. (Метод индуктивных утверждений Флойда)

Пусть даны блок-схема P и ее спецификация F = ( , y ). Выполним следующие действия:

1. Выберем точки сечения;
2. Найдем подходящий набор индуктивных утверждений;
3. Построим условия верификации для всех базовых путей.

Если все условия  верификации истинны, то блок-схема P частично-корректна относительно спецификации F.

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

 

 

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

 

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

Имеются по меньшей  мере две причины, по которым программа  с заданным предусловием 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) (_U(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) (_U(x₁, …, x_n)) inv_t((x₁, …, x_n)) – условие корректности метода индуктивных утверждений, – обратное преобразование, осуществляемое на пути в методе индуктивных утверждений, т.е.

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

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

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

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

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

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

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

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

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

 

 

Основные концепции  формализации семантики программ, аксиоматическая система Хоара

 

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

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

Верификация последовательных алгоритмов

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

φ ::= p | Øφ | (φ Ú φ).

Здесь p – базовое предложение (например, «x равно 2»), символ «Ø» – отрицание, а символ «Ú» – дизъюнкция. Другие логические связки могут быть определены следующим образом: φ Ù ψ = Ø(Øφ Ú Øψ), true = φ Ú Øφ, false = Øtrue и φ ® ψ = Øφ Ú ψ. Для простоты опустим кванторы существования и всеобщности.

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

Для построения доказательств используется формальная система – множество правил вывода. Эти правила обычно соответствуют построению программы (алгоритма). Они записываются следующим образом:

{φ} S {ψ}.

Здесь φ – предусловие, S – программный оператор, а ψ – постусловие. Тройка {φ} S {ψ} известна как тройка Хоара [13] и названа в честь одного из пионеров в области формальной верификации компьютерных программ. Существуют две интерпретации троек Хоара в зависимости от того, частичная или тотальная корректность рассматривается.

• Формула {φ} S {ψ} называется частично корректной, если каждое останавливающееся вычисление S, стартующее в состоянии, в котором выполняется φ, финиширует в состоянии, в котором выполняется ψ.
• Формула {φ} S {ψ} называется тотально корректной, если каждое вычисление S, стартующее в состоянии, в котором выполняется φ, останавливается и финиширует в состоянии, в котором выполняется ψ.

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