Методы просмотра структуры программы
Метод просмотра применяется к инспекции созданных программ независимыми экспертами и с участием самих разработчиков. На начальном этапе проектирования инспекция предполагает проверку полноты, целостности, однозначности, непротиворечивости и совместимости документов с исходными требованиями к ПС.
На этапе реализации системы инспекция состоит в анализе текста программы и проверку соблюдения требований к ней и стандартных руководящих документов технологии программирования. Эффективность инспекции заключается в том, что эксперты пытаются взглянуть на проблему "со стороны", подвергнуть ее всестороннему критическому анализу и просмотру словесных объяснений способов проектирования. Непосредственный просмотр исходного кода позволяют обнаружить ошибки в логике и в описании алгоритма.
Эти приемы позволяют на более ранних этапах проектирования обнаружить ошибки путем многократного просмотра исходных кодов. Методы просмотра не формализованы и определяются степенью квалификации экспертов группы. Основные методы рассматриваются ниже.
Метод простого структурного анализа. Он ориентирован на анализ структуры программы и потоков данных и базируется на использовании теория графов для представления структуры программы в виде графа, каждая вершина которого – это оператор, а дуга – передача управления между операторами. Согласно графу определяется достижимость вершин программы и выход потоков управления для ее завершения и обнаружение логических ошибок [5,12].
Для проведения анализа потоков данных данный граф пополняется указателями переменных, их значениями и ссылками на операторы программы. При тестировании потоков данных определяются значения предикатов в логических операторах, по которым формируются пути выполнения программы. Для прослеживания путей устанавливаются точки, в которых имеется ссылка на переменную до присвоения ей значения, либо переменной присваивается значение без ее описания, либо делается повторное описание переменной или переменной, к которой нет обращения.
Метод анализа дерева отказов. Этот метод пришел в программную инженерию из техники, в которой он широко применяется для анализа неисправностей аппаратуры. Суть метода состоит в выборе "ситуации отказа» в определенной компоненте системы, прослеживании событийных цепочек, которые могли бы привести к ее возникновению, и в построении дерева отказов, использующего предикаты и, или. С другой стороны, просматривается влияние отказа в одной компоненте на программное обеспечение в целом. При данном способе строиться дерева отказов. Данный метод применяется как на модульном уровне, так и на уровне анализа функционирования комплекса. Известен опыт его использования при разработке систем реального времени.
Метод проверки непротиворечивости.
Применяется при анализе логики программы для выявления операторов, которые никогда не используются, а также для обнаружения противоречий в логике программы. Этот метод часто называют методом анализа потоков управления на входных данных, часть из которых представляется в символьном виде. Результатом выполнения являются значения переменных, выраженные формулами над входными данными. В этом методе выделяются два вида задач:
1. Построения тестового набора данных для заданного пути, определяющего этот путь при символьном выполнении. В случае отсутствия такого набора делается заключение о нереализуемости (непротиворечивости) данного пути.
2. Определение пути, который будет пройден при заданных ограничениях на входные данные в виде некоторых областей значений входных объектов, и задание символьных значений переменных в конце пути, т.е. построение функции, которая реализует отображение входных данных в выходные.
Рассмотрим эти виды задач.
1). Символическое выполнение программа Р (Х, Y) на некоторых наборах данных D = (d1, d2, ..., dn ), D Ì Х, Х – множество входных данных программы Р.
Пронумеруем операторы программы Р. Состояние выполнения программы – это тройка
< N, pc, Z
>,
где N – номер текущего оператора программы Р, pc
(part condition) – условие выбора пути в программе (вначале это true), что является логическим выражением над D; Z
– множество пар { < zi, ei >| zi Î X Ç Y, в которых zi – переменная программы, а ei – ее значение; Y – множество промежуточных и выходных данных.
Семантика символического выполнения задается правилами оперирования символьными значениями, согласно которым арифметические вычисления заменяются алгебраическими.
Зададим семантику символического выполнения операторов через базовые конструкции языков программирования. Для императивных языков базовыми конструкциями есть операторы присваивания, перехода и условные операторы.
В операторе присваивания Z = e ( x, y), x Î X, y Î Y, в выражение e ( x, y) производится подстановка символьных значений переменных x и y, в результате чего получается выражение e (D), которое становится значением переменной z (z Î Х ÈУ). Вхождение в полученное выражение e (D) переменных из Y означает, что их значения, а также значение z не определены.
По оператору перехода управление передается оператору, помеченному соответствующей меткой. В условном операторе « если a (x, y) то В1 иначе В2 » вычисляется выражение a (x, y). Если оно определено и равно a¢ (D), то формируются логические формулы:
рс ® a’ (D ) ( 1)
рс ® Ø a’ (D) ( 2)
Если рс – ложно (false), то только одна из последних формул может быть выполнимой, тогда :
– если выполнима формула (1) , то управление передается на В1;
– если выполнима формула (2), то управление передается на В2;
– если (1), (2) не выполнимы (то есть из рс не следует ни a’ (D), ни Øa’ (D)), тогда по крайней мере один набор данных, который удовлетворяет рс и cоответствует части «то» условного оператора, а также есть набор данных, соответствующий иначе этого условного оператора.
Таким образом, образуются два пути символьного выполнения, которым соответствуют свои рс:
рс1 = рс Ù a’ (D )
рс2 = рс Ù Ø a’ (D )
Символическое выполнение, нацеленное на построение тестового набора данных, реализуется следующим алгоритмом. Пусть рс = true, тогда
– для заданного пути формируется рс согласно семантики операторов, для условного оператора семантику трактуем как преобразование рс вида (1) или (2);
– решаем обе системы уравнений (1) и (2).
Решение дает тест проверки путей программы, если такого решения нет, то это означает невыполнимость пути.
2). Определение пути при заданных ограничениях на входные данные проводится таким шагами:
– полагаем рс = b ( D), где b ( D) – входная спецификация, когда ее нет, то рс = true;
– производим символьное выполнение операторов, если встречается ветвление, то запоминается состояние в данной точке или выбирается одна из ветвей; выбирается новая спецификация и выполняется условный оператор, при котором формируется состояние программы с условием рс;
– в конце пути совокупность состояний выходных переменных определяет функцию программы и набор данных, который удовлетворяет рс и является тестом, который покрывает данный путь;
– для всех промежуточных d (х,у) с выходной спецификацией g (х,у)
делается попытка доказать выполнимость следующих логических формул:
рс ® d (х,у) и рс ® g (х,у),
где рс является значением текущего условия в данной точке программы.
Для доказательства этих формул требует провести верификацию программы на данном участке пути.
Для установления пути выражения декомпозируются на множество неравенств. Если это множество содержит некоторые несовместимости, то путь нельзя установить. В случае совместимости множеств создается множество данных, которые будут использоваться во время символьного выполнения.
Символьное тестирование применяться при определении тестовых данных для проверки отдельных путей с использованием символьных значений для реальных. При этом входные значения обозначаются символами, а операторы выполняются с использованием элементарной алгебры. Выполнение заданного пути обычно включает условные переходы, символьные выражения, до которых входят как алгебраические, так и булевские конструкции.
С целью проведения статического анализа используется различные инструменты, которые позволяют исследовать структуру программы и определить виды ошибок в программе: невыполнимые коды, неинициализированные переменные, которыми хотят воспользоваться, инициализированные, но не использованные переменные и др.
Многие отказываются от формального доказательства. Это связано с тем, например, алгоритм пузырьковой сортировки намного более простой, чем его логическое описание и доказательство, а также программы обработки нечисловых данных могут быть более трудными для понимания логики, чем числовые. Техника доказательства, которая базируется на входных утверждениях для их трансформации в выходные логические правила еще не означает, что в программе нет ошибок, поскольку нельзя распознать ошибки в программах, в интерфейсах, спецификациях, в синтаксисе и семантике ЯП или в документации.
