final-report-kuzin-2010 (1184396)

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

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

Московский государственный университет имени М. В. Ломоносова,Факультет Вычислительной математики и кибернетикиОТЧЕТ ПО ПРАКТИКУМУВерификация программного обеспечения.Итератор спискаВыполнил:Студент 528 группыКузин Сергей СергеевичПреподаватель:Доктор физ.-мат. НаукПетренко АлександрКонстантиновичМосква, 2010ОглавлениеПостановка задачи .........................................................................................................................3Описание функций и структур...................................................................................................3Постановка задачи по работе с алгоритмом ...........................................................................5Тестирование алгоритма ...............................................................................................................6Описание спецификации целевой функции ............................................................................6Обоснование выбранных ветвей функциональности.............................................................9Характеристики покрытия исходного кода реализации ......................................................10Сравнение выбранных ветвей функциональности и ветвей покрытия по исходному коду...................................................................................................................................................10Описание принципов выбора тестовых данных и их количественных характеристик .....10Оценки минимальности набора тестовых данных с точки зрения покрытия ветвей .......11Описание ошибок в реализации ............................................................................................11Верификация алгоритма .............................................................................................................12Спецификация требований ACSL ............................................................................................12Ошибки реализации алгоритма..............................................................................................15Варианты и инварианты ..........................................................................................................15Количество и классификация сгенерированных лемм ........................................................17Выводы ......................................................................................................................................17Заключение ..................................................................................................................................182Постановка задачиЦелевыми функциями для спецификации являются: алгоритм реализующий итератор подвухуровневому циклическому списку и вспомогательные функции для реализацииитератора по списку и самого списка.

Листинг кода не вставлен в этот отчет в связи с егообъемом.Описание функций и структурАлгоритм состоит из нескольких шагов, а именно: создание списка определеннойструктуры, добавление в него элементов, создания итератора на этот список и, толькопосле этого, реализация итерации по этому списку. Ниже приведено описание структурысписка:struct list_head {struct list_head *next, *prev;};struct klist {struct list_headk_list;} __attribute__ ((aligned (4)));struct klist_node {void*n_klist;struct list_headn_node;intn_ref;intdata;};struct klist_iter {struct kliststruct klist_node};*i_klist;*i_cur;Таким образом, элементы первого уровня состоят из ссылок на следующий ипредыдущий элементы этого списка.Второй уровень списка состоит из ссылки на начало списка, элемента первого уровня,количества ссылок на этот элемент и данных хранящихся в этом элементе.Далее представлен список функций с их коротким описанием:static inline void list_add(struct list_head *new, structlist_head *head) – добавляет новый элемент после head и передпервым элементом.static inline void list_add_tail(struct list_head *new, structlist_head *head) – добавляет новый элемент перед head и послепоследнего элемента.3static inline void list_del(struct list_head *entry) – убираетэлемент из списка, переставляя ссылки у предыдущего и следующегоэлемента.bool knode_dead(struct klist_node *knode) – проверяет, являетсяли данный элемент убитымstatic void knode_set_klist(struct klist_node *knode, structklist *klist) – привязывает элемент второго уровня к списку.static void knode_kill(struct klist_node *knode) - меняет адресна начало списка, что обозначает что этот элемент был удален.void klist_init(struct klist *k) – инициализирует список.static void add_head(struct klist *k, struct klist_node *n) –добавляет элемент второго уровня в начало спискаstatic void add_tail(struct klist *k, struct klist_node *n) –добавляет элемент второго уровня в конец спискаstatic void klist_node_init(struct klist *k, struct klist_node*n) – инициализирует элемент второго уровняvoid klist_add_head(struct klist_node *n, struct klist *k) –инициализирует элемент второго уровня и добавляет его в началоспискаvoid klist_add_tail(struct klist_node *n, struct klist *k) –инициализирует элемент и добавляет его в конец спискаvoid klist_add_after(struct klist_node *n, struct klist_node*pos) – инициализирует элемент и добавляет его послесуществующего элемента спискаvoid klist_add_before(struct klist_node *n, struct klist_node*pos) – инициализирует элемент и добавляет его перед существующимэлементомstatic void klist_release(struct klist_node *n) – отсоединяетэлемент от спискаstatic int klist_dec_and_del(struct klist_node *n) – уменьшаетколичество ссылок на элемент на 1 и если количество равно нулю,отсоединяет элемент от спискаstatic void klist_put(struct klist_node *n, bool kill) –уменьшает число ссылок и пытается удалить элементvoid klist_del(struct klist_node *n) – вызывает klist_put спараметром kill = true.4int klist_node_attached(struct klist_node *n) – проверяетпривязан ли элемент к списку или нетvoid klist_iter_init_node(struct klist *k, struct klist_iter *i,struct klist_node *n) – инициализирует итератор списка наопределенном элементе спискаvoid klist_iter_init(struct klist *k, struct klist_iter *i) –инициализирует итератор списка на голове спискаvoid klist_iter_exit(struct klist_iter *i) – заканчиваетитерацию, убирает ссылку с элементаstruct klist_node *to_klist_node(struct list_head *n) –возвращает ссылку на элемент содержащий данныйstruct klist_node *klist_next(struct klist_iter *i) – переходитна следующий «живой» элемент списка, уменьшая на 1 количествоссылок на текущем элементе и увеличивая на 1 количество ссылок наследующем «живом» элементе.

Итератор заканчивает работу когдадостигнут конец списка либо найден следующий «живой» элемент.Постановка задачи по работе с алгоритмом1. Необходимо формализовать требования алгоритма к входным данным.Неформально, основной алгоритм перехода к следующему элементу требуеткорректную ссылку на итератор списка. Требуется описать это в терминах языковформальных спецификаций. Кроме того, требуется описать требования к входнымданных всех вспомогательных функций2. Необходимо формализовать требования к результату выполнения алгоритма.Неформально, основной алгоритм должен выдавать следующий «живой» элементсписка, либо возвращать NULL при достижении конца списка, завершаться прикорректных параметрах и не производить некорректных действий, таких какобращение к чужой памяти и т.д.

Необходимо формализовать эти требованияТакже необходимо формализовать требования к результатам выполнениявспомогательных функций.5Тестирование алгоритмаОписание спецификации целевой функцииНа данном этапе задания спецификация формулируется в терминах встроенных типовинструмента CTesK.1. Klist_initПредусловия:Отсутствуют.Постусловия:- Список создан.2. Klist_add_headПредусловия:-Список существует, указатель не нулевой.Постусловия:-В список добавлен переданный элементБыл добавлен только один элементКоличество ссылок на этот элемент равно 1.Элемент был добавлен на свое место3. Klist_add_tailПредусловия:-Список существует, указатель не нулевой.Постусловия:-В список добавлен переданный элементБыл добавлен только один элементКоличество ссылок на этот элемент равно 1.Элемент был добавлен на свое место ( в конец списка)4.

klist_add_afterПредусловия:-Список существует, указатель не нулевой.Список не пустойСсылка указывает на существующий элемент списка6Постусловия:-В список добавлен переданный элементБыл добавлен только один элементКоличество ссылок на этот элемент равно 1.Элемент был добавлен на свое место ( после указанного элемента)5. Klist_add_beforeПредусловия:-Список существует, указатель не нулевой.Список не пустойСсылка указывает на существующий элемент спискаПостусловия:6. Klist_delВ список добавлен переданный элементБыл добавлен только один элементКоличество ссылок на этот элемент равно 1.Элемент был добавлен на свое место ( перед указанным элементом)Предусловия:-Список существует, указатель не нулевой.Список не пустойСсылка указывает на существующий элемент спискаПостусловия:-Если число ссылок на данный элемент равнялось одной, то элементсписка удаляется из негоЕсли нет, число ссылок уменьшено на 1.Был удален (понижено число ссылок), у нужного элемента7.

klist_node_attachedПредусловия:-Список существует7Постусловия:- Возвращается true если элемент принадлежит списку.8. klist_iter_init_nodeПредусловия:-Список существует, указатель не нулевой.Список не пустойСсылка указывает на существующий элемент спискаПостусловия:-Возвращен итератор на указанный элементЧисло ссылок на элемент было увеличено9. klist_iter_initПредусловия:-Список существует, указатель не нулевой.Постусловия:-Возвращен итератор на начало списка10.

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

Тип файла PDF

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

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

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