final-report-kiyko-2010 (1184395)

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

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

3Листинг кода ............................................................................................................................................ 3Описание алгоритма ............................................................................................................................... 3Постановка задачи по работе с алгоритмом ........................................................................................ 4Тестирование алгоритма ............................................................................................................................

5Описание спецификации целевой функции ......................................................................................... 5Обоснование выбранных ветвей функциональности .......................................................................... 6Характеристики покрытия исходного кода реализации ...................................................................... 6Сравнение выбранных ветвей функциональности и ветвей покрытия по исходному коду ............ 6Описание принципов выбора тестовых данных и их количественных характеристик ..................... 6Оценки минимальности набора тестовых данных с точки зрения покрытия ветвей .......................

7Описание ошибок в реализации ............................................................................................................ 7Верификация алгоритма ............................................................................................................................. 8Спецификация требований ACSL ............................................................................................................

8Ошибки реализации алгоритма ............................................................................................................. 9Варианты и инварианты.......................................................................................................................... 9Сгенерированные леммы .....................................................................................................................10Выводы ...................................................................................................................................................11Заключение ................................................................................................................................................122Постановка задачиЦелевой алгоритм задан следующим листингом кода с приведением описания егофункциональности, а именно, поиск всех вхождений подстроки x в строку y.Листинг кодаunsigned HORSPOOL(const char *y,const char *x, int n, int m, int*result) {int a, i, j, bm_bc[ASIZE];char ch, lastch;int resultSize = 0;L1:L2:L3:L4:L5:L6:/* Preprocessing */for (a = 0; a < ASIZE; a++)bm_bc[a] = m;for (j = 0; j < m - 1; j++)bm_bc[x[j]] = m - j - 1;/* Searching */lastch = x[m - 1];i = 0;while (i <= n - m) {ch = y[i + m - 1];if (ch == lastch)if (memcmp(&y[i], x, m - 1) == 0) {result[resultSize] = i;resultSize++;}i += bm_bc[ch];}return resultSize;}Описание алгоритмаИсходя из приведенного кода, был выявлен алгоритм нахождения подстроки.

Выполнениеалгоритма состоит из двух принципиально различных этапов: построение специальных структур,необходимое для эффективного поиска подстроки «x» в различных строчках «y» , и собственно,поиск.Этап1. Создание необходимых структур. Массив bm_bc, размер которого равен количествусимволов в алфавите, должен удовлетворять требованию: bm_bc[i] == m, если символа c кодом iнет в строке x (последний символ строки х не учиьывается) или bm_bc[i]==m-1-j, где j – последнийсимвол строки x c кодом i. Такое построение bm_bc позволяет утверждать, что если текущийсимвол строки y (той строки, в которой производится поиск) равен с, то последнего символастроки x не может быть ещѐ как мунимум bm_bc[c]-1 позиций.Этап 2. Поиск подстроки. Начиная с m-го символа строки y, в цикле производим следующиедействия:1.

Сравнение последнего символа x c текущим символом строки y. Если совпадают – на шаг2, нет – на шаг 32. Сравниваем оставшиеся m-1 символов с помощью функции memcmp. Если совпадают –заносим текущую позицию i в результат. Переходим на шаг 3.3. Производим сдвиг на bm_bc[y[i]] символов, так как проверка на шаге 1 точно даст ложныйрезультат для всех пропускаемых символов. Переходим на шаг 1.3Постановка задачи по работе с алгоритмом1. Необходимо формализовать требования алгоритма к входным данным.Неформально, алгоритм требует две корректные строки и буфер достаточного размера дляхранения результата.

Требуется описать это в терминах языков формальныхспецификаций.2. Необходимо формализовать требования к результату выполнения алгоритма.Неформально, алгоритм должен находить все вхождения строки x в строку y, завершатьсяпри корректных параметрах и не производить некорректных действий, таких какобращение к чужой памяти и т.д.4Тестирование алгоритмаОписание спецификации целевой функцииНа данном этапе задания спецификация формулируется в терминах встроенных типовинструмента CTesK.specificationList* horspool_spec(String* str1, String* str2)Функция принимает две строки и возвращает список позиций, с которых начинается подстрока.Медиатор осуществляет взаимно-однозначное преобразование параметров.Предусловия.pre {return (str1 != NULL) && (str2 != NULL) &&length_String(str2)!=0;}1. Передаваемые параметры должны быть корректными указателями на строки, причѐмдлина второй строки должна быть больше нуля.Постусловия.1.

Проверяем, что каждый элемент результирующего списка обозначает позицию в строке y,с которой начинает подстрока x.for( i = 0; i < size_List(horspool_spec); i++ ) {pos = value_Integer(get_List(horspool_spec, i);if(!startsWith_String(substringFrom_String(str1, pos), str2)) {traceExceptionInfo( "Bad result: not substring from returnedindex" );return false;}}2. Проверяем, что все позиции строки y, не являющиеся элементами результата, не являютсяначалами подстроки x в y. Иными словами, проверяем, что все возможные позицииподстрок содержатся в результирующем списке.for( i = 0; i < length_String(str1); i++ ) {elem = create_Integer(i);if(indexOf_List(horspool_spec, elem) != -1) {continue;}if(startsWith_String(substringFrom_String(str1, i), str2)) {traceExceptionInfo( "Bad result: skipped index" );return false;}}3.

Проверяем, что результат не содержит дубликатов.for( i = 0; i < size_List(horspool_spec); i++ ) {o = get_List(horspool_spec, i);5if(indexOf_List(horspool_spec, o) !=lastIndexOf_List(horspool_spec, o)) {traceExceptionInfo( "Bad result: all elements arebut duplicate entry exists" );return false;}correct,}Обоснование выбранных ветвей функциональностиПосле анализа алгоритма были выявлены следующие ветви функциональности , при которыхработа алгоритма происходит принципиально различным образом.1. Пустая строка y. Вне зависимости от второй строки, должен быть возвращён пустойрезультат и не должно быть ошибок.2. Строка y содержит строку x.a.

Первая строка длиннее второйb. Длины строк равны3. Строка y не содержит строку x.a. Первая строка длиннее второйb. Длины строк равныc. Вторая строка длиннее первойХарактеристики покрытия исходного кода реализацииСравнение выбранных ветвей функциональности и ветвей покрытия поисходному кодуВ ходе тестирования выяснилось, что выбранные ветви функциональности потенциально могут непокрывать метку L6, а вернее, тело соответствующего оператора if, и при 100% покрытии ветвейфункциональности, может быть 90% покрытие строк исходного кода. В связи с этим, былидобавлены тесты, покрывающие метку L6.Описание принципов выбора тестовых данных и их количественныххарактеристикИзначально тестовые данные выбирались таким образом, чтобы покрыть все ветвифункциональности. Если ветвь была покрыта – больше тестов, подпадающих под ту же ветвь, неписалось. В последствии были добавлены тесты для покрытия метки L6 (“abab”, “cab”).

Дляупрощения реализации тесты строятся методом попарного комбинирования массивов первыхстрок и вторых строк.6char* str1s[] = {"abab", ""};char* str2s[] = {"ba", "cab", "abab", "qwerty", "zxcv" };Оценки минимальности набора тестовых данных с точки зренияпокрытия ветвейВвиду метода построения тестов, существует некоторая избыточность тестов при покрытиипервой ветви функциональности. Это происходит потому, что перебираются все пары (“”, str2s[i]),хотя достаточно одной. Остальные ветви функциональности покрываются ровно одним тестом наодну ветвь, и удаление любого теста (строки из массива str2s) приведѐт к неполному покрытию.Описание ошибок в реализацииВ ходе тестирования не было выявлено ошибок в реализации алгоритма.7Верификация алгоритмаСпецификация требований ACSLДля введения пред- и постусловий были введены специальные предикаты, ниже представленыключевые из нихpredicate res_valid_precision(int *res, integer resSize, char *y,char *x, integer m) =(\forall integer respos;(0<=respos<resSize) ==> char_eq (y,x,res[respos], m));Предикат res_valid_precision проверяет, что для каждого элемента, входящего в результат,выполняется char_eq(x, y, res[respos], m)- аналог strcmp, то есть равенство символов от y +res[respos] и x на m символов вперѐд.

Характеристики

Тип файла PDF

PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

Список файлов учебной работы