final-report-sukhanova-2011 (1184404)
Текст из файла
Московский государственный университет имени М. В. ЛомоносоваФакультет вычислительной математики и кибернетикиОТЧЕТ ПО ПРАКТИКУМУВерификация программного обеспеченияФункция bitmap_weight64Выполнила:студентка 528 группыСуханова СофьяВитальевнаПреподаватель:доктор физ.-мат. наукПетренко АлександрКонстантиновичМосква 2011ОглавлениеОглавление.................................................................................................................................................2Постановка задачи.....................................................................................................................................3Тестирование алгоритма...........................................................................................................................5Описание спецификации целевой функции........................................................................................5Обоснование выбранных ветвей функциональности ........................................................................5Характеристики покрытия исходного кода реализации ....................................................................6Сравнение выбранных ветвей функциональности и ветвей покрытия по исходному коду ............6Описание принципов выбора тестовых данных и их количественных характеристик ....................6Оценки минимальности набора тестовых данных с точки зрения покрытия ветвейфункциональности и исходного кода ..................................................................................................7Описание ошибок в реализации, которые были выявлены при помощи тестирования .................7Верификация алгоритма...........................................................................................................................8Описание спецификации требований в синтаксисе ACSL ..................................................................8Описание ошибок в реализации, которые были выявлены при помощи верификации .................8Описание выбранных инвариантов и вариантов ...............................................................................8Описание и обоснование лемм num_ops_*........................................................................................9Количество и классификация сгенерированных лемм ....................................................................16Выводы, сделанные по результатам верификации ..........................................................................17Допущения, при которых алгоритм является корректным ..........................................................17Проблемы с инструментами верификации и предложения по их улучшению ..........................17Заключение .............................................................................................................................................182Постановка задачиВ исходном файле описана реализация функции, подсчитывающейколичество единиц в последовательности битов, заданной как массив чиселтипа unsigned long long int.Анализируемая функция:int bitmap_weight64(const unsigned long long *bitmap, int bits),где bitmap – массив чисел, рассматриваемый как последовательность битов,а bits – количество рассматриваемых битов из этой последовательности.Функция возвращает число типа int – количество единичных битов.Для вычисления количества единичных битов в последовательностибит bitmap сначала определяется, сколько рассматривается полных чиселтипа unsigned long long int, затем с помощью вспомогательной функцииhweight64 считается количество единичных битов в двоичной записикаждого полного числа.
Далее подсчитывается количество единиц вдвоичной записи последнего (неполного) числа, в котором рассматриваютсяне все биты. Для этого умножением на специальную маску выделяютсярассматриваемые биты, и для полученного числа вызывается функцияhweight64.Вспомогательная функция:unsigned long long int hweight64(unsigned long long int w)Данная функция возвращает количество единичных битов в двоичнойзаписи числа w.Вычисление количества единичных битов в числе w состоит из 6 шагов.На первом шаге в каждой паре битов получается число, равноеколичеству единичных битов в этой паре. На втором шаге в каждой четверкебитов получается сумма первых двух битов в четверке и последних двухбитов в четверке. Таким образом, в каждой четверке битов записано,сколько единичных битов было в этой четверке.
На третьем шаге в каждойвосьмерке битов получается сумма первых четырех битов в восьмерке ипоследних четырех битов в восьмерке. На четвертом, пятом и шестом шагахрезультат суммируется с тем же результатом, только сдвинутым на 8, 16 и 32соответственно. Таким образом, в последних восьми битах получаетсясумма всех восьми восьмерок, то есть количество единичных битов во всемчисле w.3Работа с заданной функцией включает в себя несколько этапов:1. Разработка тестов на основе формальных спецификаций.Разработка формальной спецификации функциональныхтребований к работе алгоритма на спецификационном расширенииязыка Си (SeC).•Разработка тестовых сценариев, обеспечивающих покрытие всехстрок кода реализации алгоритма, с помощью инструмента CTesK.•2.
Аналитическое доказательство корректности алгоритма.• Добавление в исходный файл (*.c) предусловий, постусловий,инвариантов и вариантов циклов целевой функции в видекомментариев в соответствии с синтаксисом ACSL.• Доказательство лемм сгенерированных инструментом Frama-Спри помощи alt-ergo и PVS.4Тестирование алгоритмаОписание спецификации целевой функцииПредусловие:Все указатели на рассматриваемые элементы массива не должны бытьnull и должны допускать корректное разыменование, и количестворассматриваемых бит не должно быть меньше нуля.Постусловие:Функция должна возвращать в качестве результата количествоединичных бит в рассматриваемой части массива.Обоснование выбранных ветвей функциональностиБыло выбрано четыре ветви функциональности:1.Количество рассматриваемых битов равно нулю.Количество рассматриваемых битов меньше, чем количество бит взаписи числа типа unsigned long long int (BITS_PER_LONG).2.Количество рассматриваемых битов кратно количеству битов в записичисла типа unsigned long long int (BITS_PER_LONG).3.Количество рассматриваемых битов не кратно количеству битов взаписи числа типа unsigned long long int (BITS_PER_LONG).4.Ветви функциональности были выбраны так, чтобы покрыть всевозможные ветви целевой функции по исходному коду:•Цикл по всем числам unsigned long long int (полным) может выполнятьсяили не выполняться - в зависимости от того, больше или меньшеколичество рассматриваемых битов количества битов в записи числа типаunsigned long long int (BITS_PER_LONG).•Проверка на то, осталось ли у нас последнее (неполное) число, в которомнадо просмотреть только часть битов, зависит от того, кратно ли числорассматриваемых битов количеству битов в записи числа типа unsignedlong long int (BITS_PER_LONG).5Характеристики покрытия исходного кода реализацииВо время тестирования было достигнуто 100% покрытие исходногокода по строкам и ветвям реализации.Сравнение выбранных ветвей функциональности и ветвейпокрытия по исходному кодуВетви функциональности были выбраны так, чтобы полностьюпокрывать все варианты поведения функции, то есть соответствуют ветвямпокрытия по исходному коду.
Было достигнуто 100% покрытие ветвейфункциональности, соответственно, было достигнуто 100% покрытие ветвейисходного кода.Описание принципов выбора тестовых данных и ихколичественных характеристикТестовые данные выбирались так, чтобы были покрыты все ветвифункциональности целевой функции.Используемые тесты:1.Количество рассматриваемых битов равно 0.Количество рассматриваемых битов равно BITS_PER_LONG-20.
ПервыеBITS_PER_LONG-30 битов заполнены последовательным чередованием 1и 0, а в битах с номерами от BITS_PER_LONG-30 до BITS_PER_LONG-21порядок чередования 1 и 0 противоположный.2.Количество рассматриваемых битов равно BITS_PER_LONG*3. ПервыеBITS_PER_LONG-30 битов заполнены последовательным чередованием 1и 0; в битах с номерами от BITS_PER_LONG-30 до BITS_PER_LONG-21порядок чередования 1 и 0 противоположный; в битах с номерами отBITS_PER_LONG-20 до BITS_PER_LONG*2 - 1 порядок чередования 1 и 0становится прежним, а в битах с номерами от BITS_PER_LONG*2 доBITS_PER_LONG*3 - 1 порядок чередования 1 и 0 снова становитсяпротивоположным.3.Количество рассматриваемых битов равно BITS_PER_LONG*3 плюс ещедва бита. Биты от 0 до BITS_PER_LONG*3 заполнены так же, как описано впункте 3, а последние рассматриваемые биты равны 1 и 0.4.6Оценки минимальности набора тестовых данных с точки зренияпокрытия ветвей функциональности и исходного кодаПредложенный набор тестовых данных является минимальным с точкизрения покрытия ветвей функциональности и, как следствие, покрытияисходного кода.Описание ошибок в реализации, которые были выявлены припомощи тестированияВ макросе, использованном в целевой функции для создания маскидля последнего числа, была обнаружена ошибка типизации.#define BITMAP_LAST_WORD_MASK(nbits)(((nbits) % BITS_PER_LONG) ?(1ULL<<((nbits) % BITS_PER_LONG))-1 : ~0ULL),/* (1UL<<((nbits) % BITS_PER_LONG))-1 : ~0UL // Error: Must be unsignedlong long instead of unsigned long */Вместо константы 1ULL стояла константа 1UL, поэтому при выполнениисдвига на число большее, чем число бит в числе типа unsigned long int,возникало переполнение, и маска получалась некорректной.
Как следствие,некорректно считалось число единичных бит в последнем (неполном) числе.Если последнее (неполное) слово по битам занимает меньшеполовины BITS_PER_LONG, то есть меньше UL, то побитовый сдвигпроисходит нормально. Но если последнее слово будет занимать большеполовины BITS_PER_LONG, то при сдвиге в BITMAP_LAST_WORD_MASKпроизойдет ошибка, и получится неверный результат. Данная ошибкаотлавливается во 2й ветви функциональности, где последнее число занимаетBITS_PER_LONG-20 бит.7Верификация алгоритмаОписание спецификации требований в синтаксисе ACSLСпецификация целевой функции bitmap_weight64:@ requires@(( bits >= 0 ) &&@( (bits%BITS_PER_LONG) ?@\valid_range(bitmap, 0, bits/BITS_PER_LONG) :@\valid_range(bitmap, 0, bits/BITS_PER_LONG-1) ));@ ensures@(\result == bit_list_hweight(@create_bit_list_from_array{Here}(bitmap, bits,0) )@);Предусловие: все указатели на рассматриваемые элементы массива недолжны быть null и должны допускать корректное разыменование, иколичество рассматриваемых бит не должно быть меньше нуля.Постусловие: функция должна возвращать в качестве результата количествоединичных бит в рассматриваемой части массива.Спецификация использующейся в bitmap_weight64 функции hweight64:@ requires \true;@ ensures@(\result == bit_list_hweight (create_bit_list (w, BITS_PER_LONG)));Постусловие: функция должна возвращать в качестве результата количествоединичных бит в числе w.Данные спецификации эквивалентны спецификации, описанной впредыдущей части.Описание ошибок в реализации, которые были выявлены припомощи верификацииВ ходе верификации ошибок в реализации выявлено не было.Описание выбранных инвариантов и вариантовВ целевой функции присутствует один цикл.
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
