Методы анализа структуры программ относятся к доказательству
правильности программ [6.20] и состоят в их инспекции независимыми
экспертами с участием самих разработчиков. Они проверяют полноту,
целостность, однозначность и непротиворечивость определений в
программе. Сущность инспекции заключается в том, что эксперты
пытаются взглянуть на программу "со стороны", подвергнуть ее
всестороннему критическому анализу, рассмотреть словесные
объяснения разработчиков о способах ее разработки. Цель инспекции -
обнаружение ошибок в логике и в исходной программе в статике.
Сквозной контроль может сопровождаться ручной имитацией выполнения
программы на выбранных тестах для получения результатов и сравнения
их с ожидаемыми. Эти приемы позволяют обнаружить ошибки при
многократном просмотре исходного кода, так они не формализованы, их
проверка зависит от степени квалификации экспертов группы.
Метод простого структурного анализа ориентирован на анализ графовой
структуры программы, в которой каждая вершина - оператор, а дуга -
передача управления между операторами. На основе графа определяется
достижимость вершин программы и существование выходов всех потоков
управления для ее завершения.
Для проведения анализа потоков данных граф расширяется специальными
указателями переменных, их значениями и ссылками на каждый оператор
программы.
При тестировании потоков данных сначала определяются значения
предикатов в операторах реализации логических условий, по которым
проходили пути выполнения программы. Затем проводится проверка
вычислений на арифметических операциях. Для прослеживания путей
программы устанавливаются точки, в которых имеются ссылки на
переменные до присвоения им значений. Переменной присваивается
значение без ее описания либо выполняется повторное описание
переменной, к которой нет обращения.
Метод символьной проверки применяется при анализе логики программы
и выявлении операторов, по которым не проходит путь вычислений, а
также при обнаружении противоречий в описаниилогики программы. Этот
метод называют методом анализа потоков управления в символьном
виде. Результат проверки - значения переменных, полученных из
выражений формул над входными потоками данных.
Метод задается следующими шагами:
1. построение тестового набора данных для заданного пути в виде
последовательности операторов символьного выполнения. В случае
невозможности построения такого набора делается заключение о
нереализуемости (противоречивости) данного пути;
2. определение пути прохождения, при котором выполняются заданные
ограничения на входные данные и символьные значения переменных.
Приведем шаги символьной проверки.
Шаг 1. Пусть - программа, выполняемая символически на наборах
данных , где и - множество входных данных.
Пронумеруем операторы программы и обозначим состояние выполнения
программы в виде тройки
где - номер текущего оператора программы , ( ) - условие выбора
пути в программе (вначале ) в виде логического выражения над
данными ; - множество пар , в которых - переменная программы, а -
ее значение; - множество промежуточных и выходных данных.
Семантика символьного выполнения задается базовыми конструкциями ЯП
и правилами оперирования символьными значениями, как
алгебраическими вычислениями. К базовым конструкциям относятся
операторы присваивания, перехода и условные операторы.
В операторе присваивания , , в выражение подставляются символьные
значения переменных и , в результате чего получается выражение ,
которое становится значением переменной . Вхождение в полученное
выражение переменных из означает, что их значения, а также значение
не определены.
Оператор перехода - это ссылка к помеченной меткой оператора
программы.
Согласно условного оператора "если то иначе " вычисляется выражение
. Если оно определено и равно , то формируются логические
формулы:
( 6.1)
( 6.2)
Если , то только одна из этих формул может быть выполнимой, а
именно если
· формула (6.1) выполнима, то управление передается на оператор
;
· формула (6.2) выполнима, то управление передается на оператор
;
· (6.1), (6.2) не выполнимы (т.е. из не следует ни , ни ), тогда
один набор данных, который удовлетворяет и соответствует части "то"
условного оператора и имеется набор данных, соответствующий
оператору после "иначе" этого условного оператора.
Таким образом, создаются два пути символьного выполнения в
соответствии с формулами: и . Получаем, что , тогда когда
· для заданного пути формируется исходя из семантики условного
оператора, преобразующего к виду (6.1) или (6.2);
· решаются системы уравнений (6.1) и (6.2) и если решения нет, то
это означает невыполнимость пути.
Шаг 2. Определение пути при заданных ограничениях на входные данные
проводится так:
· полагаем , где - входная спецификация, когда ее нет, то ;
· производим символьное выполнение операторов, если встречается
ветвление, то запоминается состояние в данной точке или выбирается
одна из ветвей; выполняется условный оператор, при котором
формируется состояние программы с условием ;
· в конце пути прохождения по программе определяется функция и
набор данных, которым удовлетворяет , покрывающий данный путь;
· для промежуточных выходной спецификации проводится доказательство
выполнимости логических формул и , где - значение текущего условия
в данной точке программы.
Доказательства этих формул можно провести верификацией данного
участка пути. Выражение формулы декомпозируется на множество
неравенств с целью определения несовместимости, мешающей
прохождению по данному пути.
При проведении статического анализа программы используются
различные инструменты, позволяющие определить ошибки в программе
(например, неинициализированные или не использованные переменные).
Кроме того, имеются способы автоматизации символьного выполнения
программ и контроля в среде языковоориентированной разработки
[6.23].