final-report-kuzin-2010 (1184396), страница 2
Текст из файла (страница 2)
klist_iter_exitПредусловия:Отсутствуют.Постусловия:-Возвращен итератор на начало спискаЧисло ссылок на элемент уменьшено на 1Если у элемента, на который указывал итератор, число ссылок равнялось1, элемент удаляется из списка11. klist_nextПредусловия:-Список существует, указатель не нулевой.Итератор указывает либо на начало списка, либо на элемент из списка8Постусловия:-Число ссылок на элемент с которого мы ушла уменьшилось на 1Если число ссылок на элемент с которого мы уходим равно 1, элементудаляется из спискаВозвращенный итератор указывает действительно на следующий«живой» элемент списка, либо на начало спискаОбоснование выбранных ветвей функциональностиПосле анализа алгоритма были выявлены различные ветви функциональности различныхфункций.
Ниже будет представлен список функций с рассматриваемыми ветвями.(Функции, в которых была лишь одна ветвь, не входят в список)1. Klist_add_head, klist_add_tailВ этих функциях рассматривалось две ветви функциональности, а именно припустом и не пустом списке.2. klist_add_after, klist_add_before, klist_del, klist_iter_init_nodeВ этих функциях рассматривались ветви функции зависящие от позиции всписке: первая позиция, последняя позиция, позиция в центре.3.
klist_node_attachedВ этой функции рассматривалось две ветви функциональности: когда элементприсоединен к списку и когда не присоединен.4. klist_nextВ этой функции рассматривались ветви функциональности зависящие от тогона какой элемент указывает итератор.9Характеристики покрытия исходного кода реализацииПокрытие исходного кода во время тестирования составляет:-100% строк исходного кода100% ветвей исходного кода100% вызовов функций исходного кодаСравнение выбранных ветвей функциональности и ветвей покрытия поисходному кодуВыбранные ветви функциональности отвечают различным вариантам поведения функции.Таким образом, каждая ветвь функциональности отвечает определенной ветви покрытияисходного кода на определенном наборе тестов.
Так как в результате было достигнуто100% покрытие, то, следовательно, каждой ветви покрытия по исходному кодусоответствует определенная ветвь функциональности, состояние системы и тестовыйнабор, на которых достигается покрытие данной ветви.Описание принципов выбора тестовых данных и их количественныххарактеристикИзначально тестовые данные выбирались таким образом, чтобы покрыть все ветвифункциональности. Если ветвь была покрыта – больше тестов, подпадающих под ту жеветвь, не писалось.
В последствии, были добавлены тесты и частично измененареализация для покрытия функциональности, при которой удалялся элемент, с которогомы уходили при использовании функции klist_next.10Оценки минимальности набора тестовых данных с точки зренияпокрытия ветвейВ связи с тем, что тестирование проходило с использованием механизма состоянийunitesk, можно предположить, что полученный набор данных не является минимальным,но он является оптимальным с точки зрения затрат времени на его создание.Описание ошибок в реализацииВ ходе тестирования были выявлена ошибка в функции klist_dec_and_del, при которойфункция удаляла элементы из списка, на которых еще находились итераторы.
Длякорректного продолжения тестирования эта ошибка была исправлена. Далее приведенкусок кода в котором была найдена ошибка://if (--n->n_ref) { <---- errorif (!(--n->n_ref)) {//<----correct code(иначе функция удаляет//элементы из списка даже если на них висититератор, что не соответствует логике программы)klist_release(n);return 1;}11Верификация алгоритмаВ связи с тем, что некоторые функции алгоритма не поддерживаются программнымобеспечением Jessie, исходный алгоритм был упрощен, и структура списка былаприведена к следующему виду:struct klist_node{struct klist_node * prev;struct klist_node * next;unsigned n_ref;int data;char dead;};struct klist {struct klist_node * k_list;};Спецификация требований ACSL1.
Knode_dead@ requires \valid(knode);@ ensures \result == knode->dead;Предусловия:- Корректность ссылки на knode, указатель допускает корректноеразыменование.Постусловия:- Результат равен knode->dead2. Klist_release@ requires \valid(n);@ ensures not_connected (n);Предусловия:- Корректность ссылки на n, указатель допускает корректноеразыменование.Постусловия:- Узел не связан с другими узлами3. Klist_dec_and_del@ requires \valid(n);@ requires (n->n_ref > 0);@ ensures (n->n_ref == \old(n->n_ref) - 1);@ ensures ((\old(n->n_ref) == 1) ==> not_connected(n));12Предусловия:- Корректность ссылки на n, указатель допускает корректноеразыменование.- Количество ссылок на узел больше нуляПостусловия:- Количество ссылок на узел уменьшено на 1- Если количество ссылок равнялось 1, то элемент не связан с другимиузлами4.
Klist_iter_init_node@ requires \valid(i);@ requires \valid(n) || n == NULL;@ ensures i->i_klist == k;@ ensures i->i_cur == n;@ ensures (n != NULL) ==> (\old(n->n_ref) + 1 == n->n_ref);Предусловия:- Корректность ссылок на n, i, указатели допускают корректноеразыменование.Постусловия:- i->i_klist == k- i->i_cur == n- Если указатель n был не нулевым, то количество ссылок на этот узелувеличено на 15. Klist_iter_init@ requires \valid(i);@ ensures i->i_klist == k;@ ensures i->i_cur == NULL;Предусловия:- Корректность ссылки на i, указатель допускает корректноеразыменование.Постусловия:- i->i_klist == k- i->i_cur == NULL6. Klist_put@ requires \valid(n);@ requires (n->n_ref > 0);@ ensures (n->n_ref == \old(n->n_ref) - 1);Предусловия:13-Корректность ссылки на n, указатель допускает корректноеразыменование.Количество ссылок на данный узел больше нуляПостусловия:- Количество ссылок на этот узел уменьшено на 17.
Klist_iter_exit@ requires \valid(i);@ requires \valid(i->i_cur) || i->i_cur == NULL;@ requires i->i_cur != NULL ==> i->i_cur->n_ref > 0;@ ensures i->i_cur == NULL;@ ensures i->i_cur != NULL ==> \old(i->i_cur->n_ref) - 1 == i->i_cur->n_ref;Предусловия:- Корректность ссылок на n, i->i_cur, указатели допускают корректноеразыменование. Указатель i->i_cur может равнятся NULL- Если i->i_cur != NULL, количество ссылок на данный узел больше нуля.Постусловия:- i->i_cur == NULL- Если указатель i->i_cur был не нулевым, то количество ссылок на этотузел уменьшено на 18. Klist_next@ requires \valid(i);@ requires@ (\forall struct klist_node * node1, * node2;@ \base_addr (node1) == \base_addr (node2));@ requires \valid(i->i_klist);@ requires \valid(i->i_klist->k_list);@ requires \valid(i->i_cur) || i->i_cur == NULL;@ requires i->i_cur != NULL ==> i->i_cur->n_ref > 0;@ ensures \result != NULL ==> \result->dead == 0;@ ensures \result == i->i_cur;@ ensures \old(i->i_cur) != NULL && \result != NULL ==> next_p (\old(i->i_cur),\result);@ ensures \old(i->i_cur) == NULL && \result != NULL ==> next_p (i->i_klist->k_list,\result);@ ensures \old(i->i_cur) != NULL && next_p (\old(i->i_cur), i->i_klist->k_list) ==>\result == NULL;@ ensures \old(i->i_cur) == NULL && next_p (i->i_klist->k_list, i->i_klist->k_list)==> \result == NULL;@ ensures \old(i->i_cur) == NULL ==> \result != i->i_klist->k_list;14@ ensures \old(i->i_cur) != NULL && \result != NULL && next_p (\old(i->i_cur),\result) ==> \result != \old(i->i_cur);@ ensures \old(i->i_cur) != NULL && \result != \old(i->i_cur) ==> \old (i->i_cur>n_ref) - 1 == \old(i->i_cur)->n_ref;@ ensures \result != NULL ==> \result->n_ref > 0;Предусловия:- Корректность ссылок на i, i->i_klist, i->i_klist->k_list, i->i_cur , указателидопускают корректное разыменование.
Указатель i->i_cur можетравняться NULL- У всех указателей один и тот же базовый адрес, они все находятся водном адресном пространстве- Если i->i_cur не равно NULL, количество ссылок на этот узел больше нуля.Постусловия:- Если в качестве результата возвращен не нулевой указатель, то значениеresult->dead == 0- result == i->i_cur- Если result!=NULL и old( i->i_cur)!=NULL, то между ними расположенытолько «мертвые» узлы- Если result!=NULL и old(i->i_cur)=NULL, то между началом списка и узломresult расположены только «мертвые» узлы- Если old(i->i_cur)!=NULL и между ним и началом списка все узлы«мертвые», то result==NULL- Если old(i->i_cur)!=NULL и все элементы списка «мертвые», тоresult==NULL- Если old(i->i_cur)!=NULL и result!=old(i->i_cur), то количество ссылок наold(i->i_cur) уменьшено на 1- Если old(i->i_cur)!=NULL, result!=NULL и между i->i_cur и result всеэлементы мертвы, то result!=i->i_curОшибки реализации алгоритмаВ ходе верификации алгоритма ошибок реализации найдено не было.Варианты и инвариантыВ функции klist_next@ loop invariant@ \valid(next) &&@ \valid(base) &&@ next_p(base, next) &&@ (i->i_cur == NULL) &&@ (\at(i->i_cur, Pre) != NULL ==> base == \at(i->i_cur, Pre)) &&15@ (\at(i->i_cur, Pre) == NULL ==> base == i->i_klist->k_list) &&@ (next_p (base, i->i_klist->k_list) ==> next->dead != 0) &&@ (\at(i->i_cur, Pre) != NULL ==> \at (i->i_cur->n_ref, Pre) - 1 == \at(i->i_cur, Pre)->n_ref);@ loop variant@ list_length (i->i_klist, next);Инварианты.1.
Корректность ссылок на next, base, указатели допускают корректное2.3.4.5.6.7.разыменование.Все элементы между next и base являются «мертвыми»В течении всего цикла i->i_cur == NULLЕсли i->i_cur до выполнения функции не равно NULL, то base равно i->i_cur довыполнения функцииЕсли i->i_cur до выполнения функции равно NULL, то base равно i->i_klist->k_listЕсли все узлы после base «мертвые», то next->dead != 0Если i->i_cur до выполнения функции не равно NULL, то значение n_ref довыполнения функции, у этого узла, на 1 меньше чем у того же узла в текущиймомент.Вариант.1.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
