final-report-chernikova-2011 (решения 2011 года)

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

31.1 Описание алгоритма ........................................................................................................................ 31.2 Задачи ............................................................................................................................................... 4Тестирование алгоритма ........................................................................................................................... 52.1 Описание спецификации целевой функции .................................................................................... 52.2 Обоснование выбранных ветвей функциональности......................................................................

52.3 Характеристики покрытия исходного кода реализации ................................................................. 62.4 Сравнение выбранных ветвей функциональности и ветвей покрытия по исходному коду .......... 62.5 Описание принципов выбора тестовых данных и их количественных характеристик................... 62.6 Оценки минимальности набора тестовых данных с точки зрения покрытия ветвей ..................... 62.7 Описание ошибок в реализации ......................................................................................................

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

73.4. Количество и классификация сгенерированных лемм................................................................... 93.5. Выводы, сделанные по результатам верификации ........................................................................ 9Заключение ..............................................................................................................................................

102Постановка задачиВ данном задании требовалось провести тестирование и верификациюфункции, сортирующей массив чисел методом вставок со сторожевымэлементом.1.1 Описание алгоритмаДанный метод отличается от обычного метода сортировки вставками наличиемспециального сторожевого элемента, который помещается в начало массиваперед сортировкой и заведомо меньше (или равен) всех остальных элементовмассива. Это позволяет уменьшить количество операций сравнения,требующихся для сортировки массива. После окончания работы с измененныммассивом следует вернуть назад первое число, которое было заменено насторожевой элемент, и вставить на нужное место в отсортированнуюпоследовательность.void insertSortGuarded(int a[], long size) {int x;long i, j;int backup = a[0];setMin(a);for ( i=1; i < size; i++) {x = a[i];for ( j=i-1; a[j] > x; j--)a[j+1] = a[j];a[j+1] = x;}for ( j=1; j<size && a[j] < backup; j++)a[j-1] = a[j];a[j-1] = backup;}void setMin(int* x){*x = INT_MIN;return;}3Функция setMin(int* x)используется для замены первого элемента массивана заведомо минимальный, далее двумя вложенными циклами выполняетсясортировка массива вставками, после чего с помощью третьего циклавставляется на нужное место сохраненный начальный элемент исходногомассива.1.2 Задачи1.

Разработка тестов на основе формальных спецификаций:• разработать формальную спецификацию функциональныхтребований к работе алгоритма на спецификационном расширении языкаСи (SeC);• разработать тестовые сценарии, обеспечивающие покрытие всехстрок кода реализации алгоритма, с помощью инструмента CTesK.2. Аналитическое доказательство корректности алгоритма:• модифицировать исходный файл (*.c) с реализацией целевойфункции, добавив туда:· предусловие и постусловие целевой функции в видекомментариев в соответствии с синтаксисом ACSL;· инварианты и варианты циклов в целевой функции в видекомментариев в соответствии с синтаксисом ACSL;• проверить какие из лемм сгенерированных инструментомFrama-С могут быть доказаны автоматически alt-ergo;• доказать оставшиеся утверждения при помощи инструмента PVS.4Тестирование алгоритма2.1 Описание спецификации целевой функцииНа данном этапе задания спецификация формулируется в терминахвстроенных типов инструмента CTesK.Specification List* insertSortGuarded_spec(List* array)Функция принимает на вход список элементов и возвращает отсортированныйсписок.Предусловие: входной массив должен быть непустымpre {return (array != NULL); }Постусловие: массив должен быть отсортирован,for(i = 1; i < size_List(insertSortGuarded_spec); i++){if (value_Integer(get_List(insertSortGuarded_spec, i - 1)) >value_Integer(get_List(insertSortGuarded_spec, i)) ){traceExceptionInfo("Result is not sorted");return false;}}и в нем должны быть те же элементы, что и в исходном – ничего лишнего недолжно появиться, ничего нужного не должно пропасть.MultiSet* array1 = create_MultiSet(&type_Integer);MultiSet* array2 = create_MultiSet(&type_Integer);for(i = 0; i < size_List(array); i++)add_MultiSet(array1, get_List(array, i));for(i = 0; i < size_List(insertSortGuarded_spec); i++)add_MultiSet(array2,get_List(insertSortGuarded_spec, i));if (!equals(array1,array2)){traceExceptionInfo("There are some lost or extravalues in result");return false;}2.2 Обоснование выбранных ветвей функциональностипустой массив (проверка предусловия)· массив из одного элемента (этот элемент будет заменен на сторожевой,далее сортировки не происходит, элемент должен быть возвращен назад –особый случай)· отсортированный массив длиной больше 1 (при этом должна происходитьтолько замена первого элемента на сторожевой и его возвращение)·5·неотсортированный массив длиной больше 12.3 Характеристики покрытия исходного кода реализацииПокрытие исходного кода во время тестирования составляет:• 100% строк исходного кода• 100% ветвей исходного кода2.4 Сравнение выбранных ветвей функциональности и ветвей покрытия поисходному кодуКаждая из выбранных ветвей функциональности соответствует некоторомуварианту поведения функции.

Так как в результате тестирования былодостигнуто полное покрытие ветвей исходного кода, то каждой ветви покрытиясоответствует некоторая ветвь функциональности.2.5 Описание принципов выбора тестовых данных и их количественныххарактеристикТестовые данные выбирались таким образом, чтобы покрыть все ветвифункциональности. Если ветвь была покрыта – больше тестов для той же ветвине писалось.2.6 Оценки минимальности набора тестовых данных с точки зренияпокрытия ветвейПолученный тестовый набор является минимальным, т.к. удаление из неголюбого теста приведёт к неполному покрытию функции.2.7 Описание ошибок в реализацииВ ходе тестирования не было выявлено ошибок в реализации функции.6Верификация алгоритма3.1 Описание спецификации требований в синтаксисе ACSL/*@requires size>0 && \valid_range(a,0,size-1);behavior sorted: ensures sorted(a,size);behavior permutation: ensures permutation{Here,Pre}(a, 0, size-1);*/Данная спецификация почти не отличается от предыдущей – дополнительнотребуется корректность указателя на массив заданного размера , и свойствосохранения элементов массива сформулировано через предикат, обозначающийперестановку.

Он определяется аксиомами, также для удобства доказательстваопределены предикаты равенства части массива в разных состояниях памяти,сдвига элементов массива вперед и назад, леммы об их связи между собой и спредикатом перестановки.Для возможности верификации сортировочной функции потребовалосьнаписать и спецификацию дополнительной:/*@requires \valid(x);assigns *x;ensures \forall int p; *x<=p;*/Она изменяет только первый элемент по заданной ссылке и гарантирует, чторезультат окажется не больше любого другого числа int.3.2 Описание ошибок в реализации, которые были выявленыпри помощи верификацииВ ходе верификации ошибок в реализации обнаружено не было.3.3 Описание инвариантов и вариантовИнварианты и вариант для внешнего цикла сортировки:/*@loop invariant 1<=i<=size && a[0]== \at(a[0],L);for sorted: loop invariant sorted(a,i);for permutation: loop invariant permutation{Here, Pre}(a,1,size1);loop variant size-i;*/Во внешнем цикле счетчик изменяется от 1 до размера массива, первыйэлемент – сторожевой – всегда остается на своем месте.

Также на i-той7итерации первые i элементов массива являются упорядоченными повозрастанию, а все элементы, кроме первого, возможно, меняются местами и неисчезают из массива. Вариант цикла очевиден.Инварианты и вариант для внутреннего цикла сортировки:/*@loop invariant (0<=j<i) && (a[0]== \at(a[0],K));for sorted: loop invariant sorted(a,i)&& (j < i-1 ==> (a[j+2] == a[j+1] && sorted(a,i+1)))&& (\forall integer p; j<p<i ==> a[p] > x);for permutation: loop invariant eq_arr{Here, K}(a,1,j) &&moved_forw_array{Here, K}(a, j+1, i)&& eq_arr{Here, K}(a,i+1,size-1)&& x==\at(a[i],K);loop variant j;*/Счетчик внутреннего цикла меняется от значения счетчика внешнего цикла-1до 0, причем второе свойство – неявное, для его доказательства и нуженинвариант о том, что первый элемент массива не изменяется.Для сортировки добавлены инварианты, прямо повторяющие условия цикла идействия в нем, для того чтобы автопрувер смог доказать более сложныесвойства упорядоченности.