final-report-akovalenko-2011 (решения 2011 года)

Московский государственный университет им. М.В. Ломоносова,Факультет вычислительной математики и кибернетикиОТЧЕТ ПО ПРАКТИКУМУВерификация программного обеспечения.Операции с битовыми множествами: перечислениеВыполнила:студентка группы №527Коваленко А.И.Преподаватель:Доктор физ.-мат. НаукПетренко Александр КонстантиновичМосква 2011ОглавлениеОглавление............................................................................................................................................2Постановка задачи................................................................................................................................31.1. Используемые типы данных.....................................................................................................31.2.

Анализируемые функции..........................................................................................................41.3. Задачи.........................................................................................................................................62. Тестирование алгоритма..................................................................................................................72.2. Обоснование выбранных ветвей функциональности.............................................................72.3.

Характеристики покрытия исходного кода реализации.........................................................82.4. Сравнение выбранных ветвей функциональности и ветвей покрытия по исходному коду..........................................................................................................................................................102.5. Описание принципов выбора тестовых данных и их количественных характеристик.......102.6. Оценки минимальности набора тестовых данных с точки зрения покрытия ветвейфункциональности и исходного кода............................................................................................112.7. Описание ошибок в реализации, которые были выявлены при помощи тестирования....123.

Верификация алгоритма.................................................................................................................133.1. Описание спецификации требований в синтаксисе ACSL.....................................................133.2. Описание ошибок в реализации, которые были выявлены при помощи верификации....143.3. Инварианты и варианты..........................................................................................................143.4. Количество и классификация сгенерированных лемм.........................................................173.5.

Выводы, сделанные по результатам верификации...............................................................174. Заключение.....................................................................................................................................192Постановка задачиВ исходных файлах описана реализации функции перечисления длябитового множества и вспомогательных функций для работы с этиммножеством. Сам алгоритм перечисления базируется на вложенном цикле– внешний цикл по фреймам битового множества, внутренний цикл – послотам (битам).1.1. Используемые типы данныхtypedef struct set_s *set_t; // указатель на битовое множествоtypedef const struct set_s *frozenset_t; // указатель на битовоемножествоtypedef unsigned int set_coord_t; // координата бита в множествеtypedef unsigned char set_frame_t; // фрейм в битовом множествеstruct set_s {unsigned int num_slots; // количество слотов в множествеunsigned int num_used_slots; // количество используемых слотов вмножествеunsigned int num_frames; // количество фреймовset_frame_t *frames; // указатель на фреймы};31.2.

Анализируемые функцииНа первом этапе необходимо было анализировать все не staticфункции.set_t set_alloc(const unsigned int num_slots);Выделяет память под битовое множество для указанного в num_slotsколичества слотов.set_t set_free(const set_t set) ;Освобождает память, выделенную для битового множества set.unsigned int set_cardinality(const frozenset_t set);Возвращает количество используемых слотов в множестве.bool_t set_has_coord(const frozenset_t set, const set_coord_t elm) ;Возвращает TRUE в случае, когда в позиции elm множества set стоит1, и FALSE в противном случае.bool_t set_add(const set_t set, const set_coord_t elm);Добавляет единичку в позицию elm в множестве set.bool_t set_remove(const set_t set, const set_coord_t elm);Обнуляет единичку из позиции elm в множестве set.4void set_fill(const set_t set, const unsigned int num_elms, constset_coord_t elm1, ...);Добавляет элементы в множество set.

Во втором параметреуказывается количество добавляемых элементов.void set_clear(const set_t set) ;Обнуляет все элементы в битовом множестве.set_t set_copy(const frozenset_t set) ;Копирует множество.bool_t set_is_subset(const frozenset_t sub, const frozenset_t sup);Проверяет, является ли множество sub подмножеством sup.bool_t set_is_equal(const frozenset_t set1, const frozenset_t set2);Проверяет два множества на эквивалентность.int set_iter(const frozenset_t set, set_coord_t *res);Возвращает количество ненулевых элементов в множестве,модифицирует массив res, записывая туда координаты ненулевыхэлементов.51.3.

Задачи1. Разработка тестов на основе формальных спецификаций:•разработать формальную спецификацию функциональныхтребований к работе алгоритма на спецификационномрасширении языка Си (SeC);•разработать тестовые сценарии, обеспечивающие покрытие всехстрок кода реализации алгоритма, с помощью инструментаCTesK.2. Аналитическое доказательство корректности алгоритма:•модифицировать исходный файл (*.c) с реализацией целевойфункции, добавив туда:oпредусловие и постусловие целевой функции в видекомментариев в соответствии с синтаксисом ACSL;oинварианты и варианты циклов в целевой функции в видекомментариев в соответствии с синтаксисом ACSL;•проверить какие из лемм сгенерированных инструментомFrama-С могут быть доказаны автоматически alt-ergo;•доказать оставшиеся утверждения при помощи инструментаPVS.62.

Тестирование алгоритма2.1. Спецификация целевой функцииint set_iter(const frozenset_t set, set_coord_t *res);• если множество set пусто, то функция возвращает 0;• если в множестве все элементы нулевые, то функция возвращает0;•функция возвращает количество ненулевых элементов битовогомножества set;• в массив res записываются координаты ненулевых элементовмножества set.2.2.

Обоснование выбранных ветвей функциональностиset_t set_free(const set_t set) ;unsigned int set_cardinality(const frozenset_t set);void set_clear(const set_t set) ;set_t set_copy(const frozenset_t set) ;int set_iter(const frozenset_t set, set_coord_t *res);• пустое множество• непустое множествоbool_t set_has_coord(const frozenset_t set, const set_coord_t elm) ;• пустое множество• нет элемента в множестве7• есть элемент в множествеbool_t set_add(const set_t set, const set_coord_t elm);bool_t set_remove(const set_t set, const set_coord_t elm);void set_fill(const set_t set, const unsigned int num_elms, constset_coord_t elm1, ...);• пустое множество• есть такой элемент в множестве• непустое множество, новый элементbool_t set_is_subset(const frozenset_t sub, const frozenset_t sup);• set и sub пустые множества• set или sub пустое множество• sub не является подмножеством set• sub подмножество setbool_t set_is_equal(const frozenset_t set1, const frozenset_t set2);• оба пустые множества• одно из них пустое множество•передаётся одно и то же множество• множества равны2.3.

Характеристики покрытия исходного кода реализацииПокрытие исходного кода во время тестирования составляет:8• 97.37% строк исходного кода• 100% ветвей исходного кода• 78.95% вызовов функций исходного кодаНе покрыто:•set_alloc called 2542 returned 100% blocks executed 80%(неуспешное выделение памяти для множества)2542: 111:if(NULL == set || NULL == frames) {branch 0 taken 100% (fallthrough)branch 1 taken 0%branch 2 taken 0% (fallthrough)branch 3 taken 100%#####: 112:call0 never executed-: 113:•abort();}set_clear called 3 returned 100% blocks executed(неуспешный вызов realloc для выделения памяти)1: 254:91%if(NULL == curr_frame) {branch 0 taken 0% (fallthrough)branch 1 taken 100%#####: 255:call0 never executed-: 256:•abort();}set_copy called 2 returned 100% blocks executed 75% (неуспешноевыделение памяти под множество)2: 285:if(NULL == set || NULL == frames) {9branch 0 taken 100% (fallthrough)branch 1 taken 0%branch 2 taken 0% (fallthrough)branch 3 taken 100%#####: 286:call0 never executed-: 287:•abort();}остальные функции возвращают returned 100% blocks executed100%2.4.

Сравнение выбранных ветвей функциональности и ветвейпокрытия по исходному кодуВетви функциональности были выбраны так, чтобы покрытьмаксимально возможное количество ветвей по исходному коду.Непокрытыми остались только неудачные попытки выделения памяти.2.5. Описание принципов выбора тестовых данных и ихколичественных характеристикТестовые данные выбирались так, чтобы покрыть максимальновозможное количество ветвей по исходному коду. Пришлось дажедобавить несколько уточнений в существующие спецификации и написатьдополнительную спецификацию для проверки функции set_is_equal() – дляпроверки на равенство тех множеств, размерности которых не совпадают,но совпадают все позиции единичек.102.6. Оценки минимальности набора тестовых данных с точкизрения покрытия ветвей функциональности и исходногокодаset_t set_free(const set_t set) ;unsigned int set_cardinality(const frozenset_t set);void set_clear(const set_t set) ;set_t set_copy(const frozenset_t set) ;int set_iter(const frozenset_t set, set_coord_t *res);• пустое множество• непустое множествоbool_t set_has_coord(const frozenset_t set, const set_coord_t elm) ;• пустое множество• нет элемента в множестве• есть элемент в множествеbool_t set_add(const set_t set, const set_coord_t elm);bool_t set_remove(const set_t set, const set_coord_t elm);void set_fill(const set_t set, const unsigned int num_elms, constset_coord_t elm1, ...);• пустое множество• есть такой элемент в множестве• непустое множество, новый элементbool_t set_is_subset(const frozenset_t sub, const frozenset_t sup);11• set и sub пустые множества• set или sub пустое множество• sub не является подмножеством set• sub подмножество setbool_t set_is_equal(const frozenset_t set1, const frozenset_t set2);• оба пустые множества• одно из них пустое множество• передаётся одно и то же множество• множества равныВсе эти варианты покрывают выбранные ветви функциональности истроки исходного кода (за исключением неуспешных попыток выделенияпамяти).2.7.

Описание ошибок в реализации, которые были выявлены припомощи тестированияПри тестировании ошибок в реализации выявлено не было. Былвыявлен недостижимый код (на входе в этот цикл num_frames всегда равно0):/* if any bits (slots) are set then total will be non-zero *//*for(; num_frames--; ++frame) {total += *frame;}*/123. Верификация алгоритмаНа втором этапе верифицировалась только функция set_iter(). Былаперенесена в отдельный файл из-за возникавших у компилятора ошибокненахождения стандартных функций (несмотря на то, что необходимыйфайл .h подключался). Такое допущение возможно в силу того, что вфункции set_iter отсутствуют вызовы других функций исходного кода.3.1.

Описание спецификации требований в синтаксисе ACSL/*@requires \valid(set)@&&set->num_framesMIN_NUM_SLOTS_PER_SET / NUM_SLOTS_PER_FRAME>=@&& \valid((set_coord_t*) res + (0..set->num_frames *NUM_SLOTS_PER_FRAME))@&& \valid(set->frames + (0..set->num_frames - 1))@&& set->num_frames < MAX_FRAMES_ON_STACK@;@ensures \old(set) == set;@ensures 0 <=NUM_SLOTS_PER_FRAME;\result<=MAX_FRAMES_ON_STACK*@ensures \forall integer i; 0 <= i < \result ==> (set>frames[get_frame(res[i])] & (1 << (NUM_SLOTS_PER_FRAME get_slot(res[i]) - 1))) != 0;@ensures \forall integer j; (0 <= j < (set->num_frames *NUM_SLOTS_PER_FRAME) && (\forall integer i; 0 <= i < \result ==>(res[i]!=j)))==>(set->frames[get_frame(j)]&(1<<(NUM_SLOTS_PER_FRAME - get_slot(j) - 1))) == 0;@*/13На вход передаётся множество, возможно пустое, но под множествообязательно выделена память, размеры его (исходя из реализации висходном коде) ограничены.В постусловиях мы гарантируем, что• исходное множество не изменится;• функция вернёт число, ограниченное максимально возможнойразмерностью исходного множества;• в массив res запишутся координаты, по которым в исходноммассиве находятся ненулевые элементы;• все остальные элементы – нулевые.В первой спецификации мы проверяли корректность работы функцийна уровне результата.