final-report-rogozhkin-2010 (1184400)

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

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

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

4Постановка задачи по работе с функцией …........................................................................................ 4Тестирование алгоритма .......................................................................................................................... 5Описание спецификации целевой функции ......................................................................................... 5Обоснование выбранных ветвей функциональности ..........................................................................

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

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

14Выводы .................................................................................................................................................... 14Заключение ................................................................................................................................................ 15Постановка задачиВ данном задании требовалось провести тестирование и верификацию набора функции strtok.Целевая функция задана следующим листингом кода с приведением описания её функциональности.Листинг кода#define NULL ((void*)0)char* strtok_r(char *s1, const char *s2, char **lasts){const char *sepp;intc, sc;char*tok;if( s1 == NULL ){if( *lasts == NULL )return NULL;}s1 = *lasts;}for( ; (c = *s1) != 0; s1++ ){for( sepp = s2 ; (sc = *sepp) != 0 ; sepp++ ){if( c == sc )break;}if( sc == 0 )break;}if( c == 0 ){*lasts = NULL;return NULL;}tok = s1++;for( ; (c = *s1) != 0; s1++ ){for( sepp = s2; (sc = *sepp) != 0; sepp++ ){if( c == sc ){*s1++ = '\0';*lasts = s1;return tok;}}}*lasts = NULL;return tok;Описание функцииФункция возвращает первый токен, содержащийся в строке и заканчивающийся одним из символовразделителей.

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

Таким образом, при последующих вызовах функция сканирует строку, возвращаянайденные токены, до тех пор пока не достигнут конец строки.Постановка задачи по работе с функцией1. Необходимо формализовать требования функции к входным данным.Неформально, функция требует корректную строку в качестве второго аргумента. Требуется описатьэто в терминах языков формальных спецификаций.2. Необходимо формализовать требования к результату выполнения функции.Неформально, функция должна возвращать первый токен, содержащийся в строке, правильнообновлять значение третьего аргумента, завершаться при корректных параметрах и не производитьнекорректных действий, таких как обращение к чужой памяти и т.д.Тестирование алгоритмаОписание спецификации целевой функцииНа данном этапе задания спецификация формулируется в терминах встроенных типов инструментаCTesK.Specification String* strtok_spec( String* s1, String* s2, char** lasts ) Функция принимает две строки идвойной указатель на char, возвращает первый токен.Медиатор осуществляет взаимно-однозначное преобразование параметров.Предусловия.pre {return (s2 != NULL);}1.

Единственным ограничением является то, что строка разделителей не может быть равна NULL.Постусловия.1. Проверяем, что в случае когда токен равен NULL либо *lasts и s1 одновременно равны NULL, либоисходная строка полностью состоит из разделителей.if (token == NULL){if ( s1 == NULL ){return true;}for( i=0; i < length_String(s1); i++ ){c = charAt_String(s1, i);if( indexOfChar_String(s2, c) == -1 ){traceExceptionInfo( "Token must be not NULL" );return false;}}}2. Все остальные случаи исходят из того, что токен не равен NULL.2.1. Проверяем, что в случае когда токен не равен NULL *lasts и s1 одновременно не могутбыть равны NULL.if ( s1 == NULL ){traceExceptionInfo( "Token must be NULL" );return false;}2.2.

Проверяем, что исходная строка содержит разделители.if ( c == 0){if ((indexOfString_String(token, s1) != 0) || (length_String(s1) != length_String(token))){traceExceptionInfo( "String doesn't contain separators" );return false;}}2.3. Проверяем, что токен содержится в исходной строке.if ( (n=indexOfString_String(s1, token)) == -1){traceExceptionInfo( "String doesn't contain token" );return false;}2.4.

Проверяем, что разделитель находится в правильном месте.for(i=0 ; i < k; i++ ){c = charAt_String(temp,i);if( lastIndexOfChar_String(s2, c) == -1 ){traceExceptionInfo( "Separator place is wrong" );return false;}}2.5. Проверяем, что токен находится в правильном месте.if (n != (k+1)){traceExceptionInfo( "Token place is wrong" );return false;}Обоснование выбранных ветвей функциональностиПосле анализа алгоритма были выявлены следующие ветви функциональности, при которых работаалгоритма происходит принципиально различным образом.1.

Первый и третий аргумент равны NULL.2. Первый аргумент не равен NULL.a. Строка состоит только из разделителей.b. В строке нет разделителей.c. Разделители в середине строки.d. Разделители в начале строки.e. Разделители и в начале, и в середине строки.3. Третий аргумент не равен NULL.Характеристики покрытия исходного кода реализацииПокрытие исходного кода во время тестирования составляет:•100% строк исходного кода•100% ветвей исходного кода•100% вызовов функций исходного кода.Сравнение выбранных ветвей функциональности и ветвей покрытия по исходномукодуКаждая из выбранных ветвей функциональности отвечает различным вариантам поведения функции.Следовательно, каждая ветвь функциональности соответствует ветви покрытия исходного кода нанекотором наборе тестов. Так как в результате тестирования было достигнуто полное покрытиеветвей исходного кода, то каждой ветви покрытия соответствует некоторая ветвь функциональности.Описание принципов выбора тестовых данных и их количественных характеристикТестовые данные выбирались таким образом, чтобы покрыть все ветви функциональности.

Если ветвьбыла покрыта – больше тестов, подпадающих под ту же ветвь, не писалось.Оценки минимальности набора тестовых данных с точки зрения покрытия ветвейПолученный тестовый набор является минимальным, т.к. удаление из него любого теста приведёт кнеполному покрытию функции.Описание ошибок в реализацииВ ходе тестирования не было выявлено ошибок в реализации функции.Верификация алгоритмаСпецификация требований ACSLДля введения пред- и постусловий были введены специальные предикаты, ниже представленыключевые из нихpredicate str_contain_chars(char* str, char* chs) =(\exists integer pos; (0<=pos<strlen(chs)) ==> str_contain_char(str, chs[pos]));Предикат str_contain_chars проверяет, есть ли в строке str символы из строки chs.predicate str_contain_only_chars(char* str, char* chs) =(\forall integer i; (0<=i<strlen(str)) ==> str_contain_char(chs, str[i]));Предикат str_contain_only_chars проверяет, что строка str состоит только из символов из строки chs.Также были сформулированы 3 леммы.lemma strlen0:\forall char* s;strlen(s)>=0;Эта лемма говорит о том, что длина любой строки больше или равна нулю.lemma strlen_ne_0:forall char* s;(*s != 0) ==> strlen(s)>0;Эта лемма говорит о том, что длина строки, у которой первый символ не равен нулевому, строгобольше нуля.

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

Тип файла PDF

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

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

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