final-report-grechanik-2010 (1184393)
Текст из файла
Московский Государственный Университет имени М.В.ЛомоносоваФакультет Вычислительной Математики и КибернетикиОтчёт по практикумуВерификация программного обеспечения. Функцияbitmap_shift_right.Выполнил:студент 528 группыГречаник Сергей АлександровичПреподаватель:доктор физ.-мат. наукПетренко Александр КонстантиновичМосква, 2010Содержание1 Постановка задачи1.1 Задача по работе с алгоритмом . . . . . .
. . . . . . . . . . . . . . . . . . . .222 Тестирование алгоритма2.1 Описание спецификации целевой функции . . . . . . . . . . . . . . . . . . . .2.1.1 Предусловие . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .2.1.2 Постусловие . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .2.2 Обоснование выбранных ветвей функциональности . . . . . . . . . . . . . . .2.3 Характеристики покрытия исходного кода реализации . . . . . . . . . . . . .2.4 Сравнение выбранных ветвей функциональности и ветвей покрытия по исходному коду . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . .2.5 Описание принципов выбора тестовых данных и их количественных характеристик . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .2.6 Оценки минимальности набора тестовых данных с точки зрения покрытияветвей функциональности и исходного кода . . . . . . . . . . . .
. . . . . . .2.7 Описание ошибок в реализации, которые были выявлены при помощи тестирования . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .4444443 Верификация алгоритма3.1 Описание спецификации требований в синтаксисе ACSL . . . . . . . . . . .3.2 Ошибки в реализации, которые были выявлены при помощи верификации3.3 Описание инвариантов и вариантов . . .
. . . . . . . . . . . . . . . . . . . .3.4 Количество и классификация сгенерированных лемм . . . . . . . . . . . . .3.5 Преобразование функции . . . . . . . . . . . . . . . . . . . . . . . . . . . . .3.6 Неисследованные пути . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . .3.7 Выводы, сделанные по результатам верификации . . . . . . . . . . . . . . .666677884 Заключение.......55551011Постановка задачиЦелевой алгоритм осуществляет сдвиг вправо битового массива. Битовый массив представлен в виде массива чисел типа unsigned long таким образом, что он является конкатенацией битовых представлений соответствующих чисел.void __bitmap_shift_right(unsigned long *dst,const unsigned long *src, int shift, int bits){int k, lim = BITS_TO_LONGS(bits), left = bits % BITS_PER_LONG;int off = shift/BITS_PER_LONG, rem = shift % BITS_PER_LONG;unsigned long mask = (1UL << left) - 1;for (k = 0; off + k < lim; ++k) {unsigned long upper, lower;if (!rem || off + k + 1 >= lim)upper = 0;else {upper = src[off + k + 1];if (off + k + 1 == lim - 1 && left)upper &= mask;}lower = src[off + k];if (left && off + k == lim - 1)lower &= mask;dst[k] = upper << (BITS_PER_LONG - rem) | lower >> rem;if (left && k == lim - 1)dst[k] &= mask;}if (off)memzero(&dst[lim - off], off);}Алгоритм работает следующим образом:1.
Определяется, какое количество элементов нового массива-представления не будутзаведомо нулевыми.2. Для каждого такого элемента считается его значение как некоторая функция отсдвига, количества бит и двух соседних элементов исходного массива-представления.3. Оставшиеся элементы заполняются нулями.1.1Задача по работе с алгоритмом1.
Разработка тестов на основе формальных спецификаций.• Разработка формальной спецификации функциональных требований к работеалгоритма на спецификационном расширении языка Си (SeC).2• Разработка тестовых сценариев, обеспечивающих покрытие всех строк кода реализации алгоритма, с помощью инструмента CTesK.2. Аналитическое доказательство корректности алгоритма.• Добавление в исходный файл с реализацией целевой функции– предусловий и постусловий целевой функции в виде комментариев в соответствии с синтаксисом ACSL– инвариантов и вариантов циклов в целевой функции в виде комментариевв соответствии с синтаксисом ACSL• Проверка того, какие из лемм, сгенерированных инструментом Frama-С, могутбыть доказаны автоматически.• Доказательство оставшихся утверждений при помощи инструмента PVS.32Тестирование алгоритма2.1Описание спецификации целевой функцииvoid __bitmap_shift_right(unsigned long *dst,const unsigned long *src,int shift,int bits);2.1.1Предусловие• Входной массив должен быть битовым массивом длины не менее bits.• Длина массива (bits) должна быть неотрицательной.• Величина сдвига (shift) должна быть неотрицательной и не должна превышатьдлину массива.2.1.2Постусловие• i-й элемент результирующего массива должен быть равен (i + shift)-му элементувходного массива, если он существует, и нулю в противном случае.2.2Обоснование выбранных ветвей функциональностиБыли выбраны следующие ветви функциональности:• Длина массива 0, сдвиг 0.• Длина массива ненулевая, сдвиг 0.• Длина массива ненулевая, сдвиг ненулевой и не равен длине массива.• Длина массива ненулевая, сдвиг равен длине массива.Ветви были выбраны на основе структуры множества допустимых входных параметров.2.3Характеристики покрытия исходного кода реализацииПокрытие исходного кода во время тестирования составляет:• 100% строк исходного кода.• 100% ветвей исходного кода.• 100% вызовов функций исходного кода.42.4Сравнение выбранных ветвей функциональности и ветвей покрытия по исходному кодуВыбранные ветви функциональности соответствуют более высокоуровневому взглядуна алгоритм, поэтому практически ортогональны ветвям покрытия по исходному коду.2.5Описание принципов выбора тестовых данных и их количественных характеристикТестовые данные формировались при помощи отображения множества троек целыхчисел (length, prefix , shift) в домен функции следующим образом:• Входной битовый массив имеет длину length, первые prefix его элементов равны 1,остальные 0• bits = length• shift = shiftНабор троек (length, prefix , shift) формировался следующим образом:• length пробегает от 0 до 3 · BITS_PER_LONG с шагом BITS_PER_LONG/2• prefix пробегает от max(0, length−2·BITS_PER_LONG) до length с шагом BITS_PER_LONG/4• shift пробегает от 0 до length с шагом 1(BITS_PER_LONG - количество бит в unsigned long)Выбор тестовых данных был обусловлен тем, что работа алгоритма сильно зависит отвыравнивания по BITS_PER_LONG.2.6Оценки минимальности набора тестовых данных с точки зрения покрытия ветвей функциональности и исходного кодаНабор тестовых данных не является минимальным, так как его мощность превышаетколичество ветвей функциональности или исходного кода.2.7Описание ошибок в реализации, которые были выявлены припомощи тестированияОшибки в реализации не были выявлены.53Верификация алгоритма3.1Описание спецификации требований в синтаксисе ACSLrequires bits >= 0 && shit >= 0 && shit <= bits&& \valid_range(dst, 0, (bits+31)/32)&& \valid_range(src, 0, (bits+31)/32)&& \base_addr(src) != \base_addr(dst)&& bits + 31 <= 2147483647;ensures same_bits(src, dst, shit, 0, bits);Данная спецификация отличается от предыдущей наличием ограничения на максимальное количество бит, чтобы не произошло арифметическое переполнение.Определения вспомогательных функций:logic integer bit_at{L}(unsigned long* a, integer n, integer k) =k < n ? (a[k / BITS_PER_LONG] >> (k % BITS_PER_LONG)) & 1 : 0;predicate same_bits{L}(unsigned long* a, unsigned long* b,integer sa, integer sb, integer n) =\forall integer k;0 <= k < n ==> bit_at(a, n, sa + k) == bit_at(b, n, sb + k);3.2Ошибки в реализации, которые были выявлены при помощиверификацииБыла выявлена ошибка в следующем операторе:dst[k] = upper << (BITS_PER_LONG - rem) | lower >> rem;Если rem равен 0 (т.е.
сдвиг происходит на количество бит кратное BITS_PER_LONG, топроисходит сдвиг влево на BITS_PER_LONG. Это число равно битовой длине значений типарезультата, а поэтому сдвиг на данное число по стандарту может приводить к неопределённому поведению.3.3Описание инвариантов и вариантовИнвариант цикла выглядит следующим образом:loop invariantk >= 0 &&off + k <= 2147483647 &&k <= lim &&k + 1 <= 2147483647 &&off + k >= 0 &&(\forall integer n; (0 <= n < k) ==>(dst[n] == f(src, shit, bits, lim, left, off, rem, mask, n)));Первые 5 инвариантов устанавливают ограничения на итерационную переменную k.Они вводились по мере возникновения трудностей у автоматического прувера.Последний инвариант описывает, какими значениями заполняется массив dst.Вариант цикла очевиден и записывается следующим образом:loop variant lim - k;63.4Количество и классификация сгенерированных леммТолько для функции __bitmap_shift_right было сгенерировано:• Условия верификации: 24• Условия корректности: 91• Условия завершимости: 2Всего (в том числе и для вспомогательных функций) было сгенерировано 197 лемм.Также было введено 26 вспомогательных лемм.3.5Преобразование функцииИсходная функция содержала большое количество выражений типа bool, что приводило к экспоненциальному увеличению количества генерируемых лемм (более тысячи).Из-за этого возрастало время автоматического доказательства лемм, а также время разбора pvs-файла.
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
