final-report-khairulin-2010 (1184402)
Текст из файла
Московский государственный университет им. М.В. Ломоносова,Факультет вычислительной математики и кибернетикиОТЧЕТ ПО ПРАКТИКУМУВерификация программного обеспечения.Быстрый алгоритм поиска подстроки Бойера-МураВыполнил:студент группы №527Хайрулин В.А.Преподаватель:Доктор физ.-мат. НаукПетренко Александр КонстантиновичМосква 2010Оглавление 1.
Постановка задачи............................................................................................... 3 1.1 Описание принципа работы алгоритма .............................................................................3 1.2 Используемые типы данных ...............................................................................................3 1.3 Анализируемые функции ....................................................................................................4 1.4 Задачи: ..................................................................................................................................4 2.
Тестирование алгоритма ..................................................................................... 5 2.1 Постусловие целевой функции ..........................................................................................5 2.2 Обоснование выбранных ветвей функциональности.......................................................5 2.3 Характеристики покрытия исходного кода реализации ..................................................5 2.4 Описание принципов работы тестовых данных и их количественных характеристик 5 2.5 Описание ошибок в реализации, которые были выявлены при помощи тестирования.....................................................................................................................................................5 3.
Верификация алгоритма ..................................................................................... 6 3.1 Описание спецификации требований в синтаксисе ACSL ..............................................6 3.1.1 int subpattern(const char *pattern, int i, int j, int g) .......................................................6 3.1.2 void compute_prefix_tbl(struct ts_bm *bm) ..................................................................6 3.1.3 void bm_init(struct ts_bm *bm, const char *pattern, int len) .........................................6 3.1.4 void search_init(struct ts_state* state, char* text, int text_len) ......................................6 3.1.5 int bm_find(struct ts_bm *bm, struct ts_state *state) .....................................................6 3.1.6 int bm_search(char* pattern, int pattern_len, char* text, int text_len) ...........................6 3.2 Описание ошибок в реализации, которые были выявлены при помощи верификации.....................................................................................................................................................7 3.3 Количество и классификация сгенерированных лемм ....................................................7 3.4 Выводы, сделанные по результатам верификации...........................................................7 3.4.1 Допущения, при которых алгоритм является корректным ......................................7 3.4.2 Проблемы с инструментами верификации и предложения по их улучшению ......7 4.
Заключение .......................................................................................................... 9 21. Постановка задачиАлгоритм Бойера-Мура поиска строки считается наиболее быстрым средиалгоритмов общего назначения, предназначенных для поиска подстроки в строке. Былразработан Робертом Бойером (англ. Robert S. Boyer) и Джеем Муром (англ. J StrotherMoore) в 1977 году.
Преимущество этого алгоритма в том, что ценой некоторогоколичества предварительных вычислений над шаблоном (но не над строкой, в которойведётся поиск) шаблон сравнивается с исходным текстом не во всех позициях — частьпроверок пропускаются как заведомо не дающие результата.1.1 Описание принципа работы алгоритмаАлгоритм основан на трёх идеях.1.
Сканирование слева направо, сравнение справа налево. Совмещается начало текста(строки) и шаблона, проверка начинается с последнего символа шаблона. Если символысовпадают, производится сравнение предпоследнего символа шаблона и т. д. Если всесимволы шаблона совпали с наложенными символами строки, значит, подстрока найдена,и поиск окончен.Если же какой-то символ шаблона не совпадает с соответствующим символом строки,шаблон сдвигается на несколько символов вправо, и проверка снова начинается споследнего символа.
Эти «несколько» вычисляются по двум эвристикам.2. Эвристика стоп-символа. В таблице стоп-символов указывается последняя позиция вшаблоне pattern (исключая последнюю букву) каждого из символов алфавита3. Эвристика совпавшего суффикса. Если при сравнении строки и шаблона совпалоодин или больше символов, шаблон сдвигается в зависимости от того, какой суффикссовпал. Для каждого возможного суффикса S шаблона pattern указываем наименьшуювеличину, на которую нужно сдвинуть вправо шаблон, чтобы он снова совпал с S.
Еслитакой сдвиг невозможен, ставится |pattern|1.2 Используемые типы данныхФункции, реализующий алгоритма Бойера-Мура используют следующие структурыданных:struct ts_state{int len;const char};*data;struct ts_bm{const char *pattern;int patlen;int bad_shft[ASIZE];int *good_shft;};//Длина текста, в котором осуществляется поиск//Текст, в котором осуществляется поиск//Искомая подстрока//Длина искомой подстроки шаблона//Таблица стоп-символов//Таблица суффиксов31.3 Анализируемые функции• int subpattern(const char *pattern, int i, int j, int g)Проверяет, дает ли смещение i-j совпавший суффикс, для вычисления таблицысуффиксов• void compute_prefix_tbl(struct ts_bm *bm)Вычисляет таблицу стоп-символов и таблицу суффиксов• void bm_init(struct ts_bm *bm, const char *pattern, int len)Выделяет память под таблицу суффиксов и запускает compute_prefix_tbl дляинициализации таблиц• void search_init(struct ts_state* state, char* text, int text_len)Функция инициализирует структуру state• int bm_find(struct ts_bm *bm, struct ts_state *state)Ищем подстроку, используя сформированные таблицы стоп-символов исуффиксов.• int bm_search(char* pattern, int pattern_len, char* text, int text_len)Основная функция поиска1.4 Задачи:1.
Разработка тестов на основе формальных спецификаций••разработать формальную спецификацию функциональных требований к работеалгоритма на спецификационном расширении языка Си (SeC);разработать тестовые сценарии, обеспечивающие покрытие всех строк кодареализации алгоритма, с помощью инструмента CTesK.2. Аналитическое доказательство корректности алгоритма• Модифицировать исходный файл (*.c) с реализацией Вашей целевойфункции, добавив туда:a. Предусловие и постусловие целевой функции в виде комментариев всоответствии с синтаксисом ACSL.b. Инварианты и варианты циклов в целевой функции в виде комментариевв соответствии с синтаксисом ACSL.• Проверить какие из лемм сгенерированных инструментом Frama-С могутбыть доказаны автоматически alt-ergo:• Доказать оставшиеся утверждения при помощи инструмента PVS.42.
Тестирование алгоритма2.1 Постусловие целевой функцииint bm_search(char* pattern, int pattern_len, char* text, int text_len)Если в строке text не содержится подстрока pattern, то результатом работы функциидолжно стать значение -1Если в строке text содержится подстрока pattern, то результатом работы функции должнабыть первая позиция искомой подстроки pattern в строке text.Нумерация символов в строке ведется с 02.2 Обоснование выбранных ветвей функциональности1. Позиция искомой подстроки в строке.Были выделены следующие позиции:• Первая позиция.
Искомая подстрока совпадает с началом строки.• Отсутствующая позиция. Искомая подстрока не содержится в строке.• Позиция внутри строки. Искомая подстрока есть где-то внутри строки2. Тривиальность таблицы суффиксов• Тривиальная таблица суффиксов. Все значения в таблице суффиксов равныдлине искомой подстроки• Нетривиальная таблица суффиксов. Существуют значения в таблицесуффиксов, отличные от длины искомой подстроки2.3 Характеристики покрытия исходного кода реализацииПокрытие исходного кода во время тестирования составляет:• 100% строк исходного кода• 100% ветвей исходного кода• 100% вызовов функций исходного кода2.4 Описание принципов работы тестовых данных и ихколичественных характеристикТесты были подобраны таким образом, чтобы обеспечить 100% покрытие ветвейфункциональности.
Это обеспечило и 100% покрытие строк исходного кода. Удалениелюбого из тестов уменьшает покрытие ветвей функциональности и исходного кода.2.5 Описание ошибок в реализации, которые были выявленыпри помощи тестированияВ ходе тестирования ошибок в реализации выявлено не было53. Верификация алгоритма3.1 Описание спецификации требований в синтаксисе ACSL3.1.1 int subpattern(const char *pattern, int i, int j, int g)requires good_string(pattern, i+g) && (i > 0) && (g > 0) && (1-g <= j <= i-1);ensures (!\result ==> !is_suffix_shift(pattern, \old(i)+\old(g), \old(g), \old(i) - \old(j)));ensures (\result ==> is_suffix_shift(pattern, \old(i)+\old(g), \old(g), \old(i) - \old(j)));Постусловием является проверка корректности определения суффикса3.1.2 void compute_prefix_tbl(struct ts_bm *bm)requires \valid((struct ts_bm*)bm) && good_string(bm->pattern, bm->patlen)&& \valid(bm->good_shft + (0..bm->patlen-1))&& \valid(bm->bad_shft + (0..(ASIZE-1)));ensures good_bm(bm);Функция требует корректно определенную строку pattern, а также корректные указателина таблицы стоп-символов и суффиксов.Постусловием является корректная структура bm.3.1.3 void bm_init(struct ts_bm *bm, const char *pattern, int len)requires good_string(pattern, len) && \valid((struct ts_bm*) bm) && \valid(bm->bad_shft +(0..(ASIZE-1)));ensures good_bm(bm) && (bm->pattern == pattern) && (bm->patlen == len);Функция требует корректно определенную строку pattern.Постусловием является корректно определенная структура bm, для которой bm->pattern иbm->patlen совпадают с переменными pattern и len3.1.4 void search_init(struct ts_state* state, char* text, int text_len)requires good_string(text, text_len) && \valid((struct ts_state*)state);ensures good_state(state) && (state->data == text) && (state->len == text_len);Функция требует корректно определенную строку text.Постусловием является корректно определенная структура state, для которой state->data иstate->len совпадают с переменными text и text_len3.1.5 int bm_find(struct ts_bm *bm, struct ts_state *state)requires good_bm(bm) && good_state(state);ensures \result == -1 ==> non_substring(bm->pattern, bm->patlen, state->data, state->len);ensures \result >= 0 ==> is_first_substring(bm->pattern, bm->patlen, state->data, state->len,\result);Функция требует корректно определенные структуры, описанные в пункте 1.2Постусловием является проверка корректности поиска подстроки bm->pattern в строкеstate->data.3.1.6 int bm_search(char* pattern, int pattern_len, char* text, int text_len)requires good_string(pattern, pattern_len) && good_string(text, text_len);ensures \result == -1 ==> non_substring(pattern, pattern_len, text, text_len);ensures \result >= 0 ==> is_first_substring(pattern, pattern_len, text, text_len, \result);Функция требует корректно заданные строки pattern и text.Постусловием является проверка корректности поиска подстроки pattern в строке text.63.2 Описание ошибок в реализации, которые были выявленыпри помощи верификацииВ ходе верификации ошибок в реализации обнаружено не было.3.3 Количество и классификация сгенерированных лемм• int subpattern(const char *pattern, int i, int j, int g)Всего: 88Условия корректности: 37Условия верификации: 48Условия завершимости: 3• void compute_prefix_tbl(struct ts_bm *bm)Всего: 133Условия корректности: 43Условия верификации: 77Условия завершимости: 13• void bm_init(struct ts_bm *bm, const char *pattern, int len)Всего: 20Условия корректности: 18Условия верификации: 2• void search_init(struct ts_state* state, char* text, int text_len)Всего: 5Условия корректности: 2Условия верификации: 3• int bm_find(struct ts_bm *bm, struct ts_state *state)Всего: 78Условия корректности: 35Условия верификации: 36Условия завершимости: 7• int bm_search(char* pattern, int pattern_len, char* text, int text_len)Всего: 13Условия корректности: 2Условия верификации: 113.4 Выводы, сделанные по результатам верификации3.4.1 Допущения, при которых алгоритм является корректнымГлавное допущение, при котором алгоритм является корректным - ограничениедлины строки.
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
