Методы и средства инженерии программного обеспечения



         

Методы просмотра структуры программы - часть 4


– если (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 (х,у),

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

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


Содержание  Назад  Вперед