final-report-kononov-2010 (решения 2010 года)

Московский государственный университетимени М. В. ЛомоносоваФакультет Вычислительной математики и кибернетикиКафедра Системного программированияОТЧЕТ ПО ПРАКТИКУМУВерификация программного обеспечения.Функция бинарного поиска bsearchВыполнил: студент 528 группыКононов Алексей ИгоревичРуководитель практикидоктор физ.-мат. наукПетренко Александр КонстантиновичМосква2010Содержание1.2.Постановка задачи ...................................................................................................................................

31.1Алгоритм работы функции bsearch ............................................................................................ 31.2Задачи по работе с алгоритмом ..................................................................................................... 4Тестирование алгоритма .........................................................................................................................

52.1Описание спецификации целевой функции.................................................................................. 52.2Обоснование выбранных ветвей функциональности .................................................................. 52.3Характеристики покрытия исходного кода реализации .............................................................. 52.4Сравнение выбранных ветвей функциональности и ветвей покрытия по исходному коду ..... 52.5Описание принципов выбора тестовых данных и их количественных характеристик ............. 52.6Оценки минимальности набора тестовых данных с точки зрения покрытия ветвейфункциональности и исходного кода ........................................................................................................

62.73.4.Описание ошибок в реализации, которые были выявлении при помощи тестирования ........ 6Верификация алгоритма ......................................................................................................................... 73.1Описание спецификации требований в синтаксисе ACSL ............................................................ 73.2Описание ошибок в реализации, которые были выявлены при помощи верификации ..........

73.3Описание выбранных инвариантов и вариантов.......................................................................... 73.4Количество и классификация сгенерированных лемм ................................................................ 73.5Выводы, сделанные по результатам верификации ...................................................................... 8Заключение .............................................................................................................................................. 921.

Постановка задачиВ данном задании требовалось провести тестирование и верификацию функции бинарного поиска. На рисунке 1 предоставлен код исходной функции бинарного поиска bseacrh.#define NULL ((void*)0)int* bsearch(int* base, int nmemb, int key){int l = 0;int h = nmemb - 1;while (l <= h){int m = (l + h)/2;int mVal = base[m];if (mVal < key)l = m + 1;elseif (mVal > key)h = m - 1;elsereturn (base + m); // key found}return NULL; // key not found.}Рисунок 1. Исходный код функции bsearch.1.1 Алгоритм работы функции bsearchКак можно увидеть из исходного кода на рисунке 1, на вход функции передается 3 параметра:1) int* base – указатель на начало массива объектов типа int, в котором эти объектыдолжны быть упорядочены по возрастанию;2) int nmemb – количество объектов в массиве, на который указывает параметр base;3) int key – объект типа int, поиск которого необходимо провести в массиве.Возвращаемое значение тестируемой функции может принимать два типа значений:1) Если элемент key содержится в массиве base, то возвращаемое значение должно бытьравно указателю на элемент массива, значение которого равно key;2) Если элемент key отсутствует в массиве base, то возвращаемое значение должно бытьравно NULL.Стоит отметить, что в функции не производится проверка на корректность и адекватностьвходных параметров.Алгоритм работы функции на естественном языке можно описать следующим образом:1) Инициализация границ массива, в пределах которого происходит поиск элемента key,границами переданного массива.2) Если левая граница поиска меньше или равна правой, то переходим на шаг 3, иначе заканчиваем работу функции и возвращаем NULL.3) Сравниваем значение элемента mVal массива base, находящегося посередине между границами поиска, со значением элемента key.

В зависимости от результата сравнения, алгоритм может продолжить работу по одному из следующих сценариев:33.1) Если mVal меньше key, то сдвигаем левую границу поиска на середину плюс один ипереходим на шаг 2;3.2) Если mVal больше key, то сдвигаем правую границу поиска на середину минус один ипереходим на шаг 2;3.3) Иначе mVal равно key, следовательно, функция нашла нужный элемент и возвращаетуказатель на элемент массива base с индексом, равным значению середины границы поиска.1.2 Задачи по работе с алгоритмомЗадача по работе с алгоритмом состоит из следующих этапов:1) Разработка тестов на основе формальных спецификаций.1) Разработать формальную спецификацию функциональных требований к работе алгоритма на спецификационном расширении языка Си (Sec).2) Разработать тестовые сценарии, обеспечивающие покрытие всех строк кода реализации алгоритма, с помощью инструмента CTesK.2) Аналитическое доказательство корректности алгоритма.2.1) Модифицировать исходной файл с реализацией целевой функции, добавив туда: Предусловие и постусловие целевой функции в виде комментариев в соответствии ссинтаксисом ACSL. Инварианты и варианты циклов в целевой функции в виде комментариев в соответствии с синтаксисом ASCL.2.2) Проверить, какие из лемм, сгенерированных инструментом Frama-С, могут быть доказаны автоматически alt-ergo.2.3) Доказать оставшиеся утверждения при помощи инструмента PVS.42.

Тестирование алгоритма2.1 Описание спецификации целевой функцииПредусловие: проверка на упорядоченность входного массива.Постусловие:1) Если результат функции не равен NULL, то:1.1) Проверка на то, что возвращенный указатель указывает на элемент равный key.1.2) Проверка на то, что возвращенный указатель указывает на элемент массива base.2) Если результат функции равен NULL, то проверка на то, что в массиве base нет элемента,значение которого равно key.2.2 Обоснование выбранных ветвей функциональностиБыли выбраны следующие ветви функциональности:1)2)3)4)Поиск объекта в пустом массиве.Поиск объекта в массиве, содержащим только один объект с таким же значением.Поиск объекта в массиве, содержащим несколько объектов с таким же значением.Поиск объекта в массиве, не содержащим объекта с таким же значением.Данные, которые использовались при реализации описанных ветвей функциональности, полностью покрывают CFG программы.2.3 Характеристики покрытия исходного кода реализацииПокрытие исходного кода во время тестирования составляет:100 % строк исходного кода;100 % ветвей исходного кода;100 % вызовов функций исходного кода.2.4 Сравнение выбранных ветвей функциональности и ветвей покрытияпо исходному кодуКак было сказано выше, выбранные ветви функциональности отвечают различным вариантамповедения функции.

Таким образом, каждая ветвь функциональности отвечает определенной ветвипокрытия исходного кода на определённом наборе тестов. Так как в результате было достигнутополное покрытие, то, следовательно, каждой ветви покрытия по исходному коду соответствует определённая ветвь функциональности, состояние системы и тестовый набор, на которых достигается покрытие данной ветви.2.5 Описание принципов выбора тестовых данных и их количественныххарактеристикКак видно из алгоритма работы функции, описанном в пункте 1.2, основная часть работы функции заключается в деление исследуемой области поиска заданного объекта на две, равные по длинеили длины которых отличаются не более чем на 1, части и выбора той части, в которой может содержаться данный объект. Так как переданный массив, должен быть упорядочен, то выбор области поиска однозначен. Поэтому необходимо было разработать тестовые данные, которые требовали бы отфункции разные выборы области поиска.

Например, на одних тестовых данных функция выбиралаобласть поиска, находящуюся слева от середины области, а на других тестовых данных функция вы5бирала бы другую область, либо на одних тестовых данных в процессе работы функции выбиралисьбы разные области поиска.Разработать тестовые данные, отвечающие принципам, описанным выше, не представлялосьсложным. Так как работа функции имела похожее поведение на данных (массивах) с большим количеством элементов, так и с маленьким, то можно было ограничиться данными с малым количествомэлементов массива.2.6 Оценки минимальности набора тестовых данных с точки зрения покрытия ветвей функциональности и исходного кодаБыл разработан набор тестовых данных больше, чем минимально необходимый, так как былотребование определить не менее 4-х ветвей функциональности адекватных для целевой функции.2.7 Описание ошибок в реализации, которые были выявлении при помощи тестированияПри тестировании ошибок в реализации выявлено не было.63.

Верификация алгоритма3.1 Описание спецификации требований в синтаксисе ACSLrequires nmemb >= 0 &&\valid_range(base, 0, nmemb-1) &&\forall integer k1, integer k2; 0 <= k1 < k2 <= nmemb-1 ==>base[k1] <= base[k2];assigns \nothing;behavior success:ensures \result != NULL ==> \exists integer i; 0 <= i < nmemb ==>(base[i] == key && base + i == \result);behavior failure:ensures \result == NULL ==> \forall integer i; 0 <= i < nmemb ==>base[i] != key;Данная спецификация эквивалентна спецификации, описанной в предыдущей части, за исключением того, что здесь дополнительно проверяется, что размер массива больше либо равен нулю ичто в указанном диапазоне указатели можно разыменовывать.3.2 Описание ошибок в реализации, которые были выявлены при помощи верификацииБыла выявлена ошибка (arithmetic overflow), связанная с возможностью переполнения переменной m типа int.

Данная ошибка возникла бы в случае, когда сумма переменных l и h типа int былабы больше чем INT_MAX. Такая ситуация могла возникнуть, например, в случае, когда массив имеетразмер равный INT_MAX-1, а элемент, который необходимо найти, расположен последним в данном массиве. Тогда в процессе сужения границ поиска, левая граница l будет приближаться к правой границе h, которая всегда будет равна размеру массива, то есть INT_MAX-1.