final-report-sukhanova-2011 (1184403), страница 3
Текст из файла (страница 3)
Если послевыполнения третьего шага в восьмерки бит записались числа единичных битв этих восьмерках в числе w, то число в восьмерке будет равно сумме чиселиз этой и следующей восьмерки в исходном числе w.Лемма num_ops_for_step5:@lemma num_ops_for_step5:@\forall unsigned long long res;@(((\forall integer i;@( (0 <= i < 7) ==>@read_num_from_bits(create_bit_list(res,BITS_PER_LONG), 8*i, 8)<=16)@)@&&@( 8 >= read_num_from_bits(create_bit_list@(res, BITS_PER_LONG), 8*7, 8)))@==>@((\forall integer i1;@( (0 <= i1 < 6) ==>@read_num_from_bits(create_bit_list((res + (res >> 16)), BITS_PER_LONG), 8*i1, 8) ==@read_num_from_bits(create_bit_list@(res, BITS_PER_LONG), 8*i1, 8) +@read_num_from_bits(create_bit_list@(res,BITS_PER_LONG), 8*i1+16, 8) )@)@&&@( 16 >= read_num_from_bits(create_bit_list@((res + (res >> 16)), BITS_PER_LONG), 8*6, 8) ==13@@@@@@@@@read_num_from_bits(create_bit_list(res, BITS_PER_LONG), 8*6, 8) )&&( 8 >= read_num_from_bits(create_bit_list((res + (res >> 16)), BITS_PER_LONG), 8*7, 8) ==read_num_from_bits(create_bit_list(res, BITS_PER_LONG), 8*7, 8) )));В данной лемме говорится о том, что если в каждой восьмерке битов,кроме последней, в res закодировано число, меньшее или равное 16, а впоследней восьмерке – меньшее или равное 8, то к каждой восьмерке битоврезультата, полученного битовыми операциями на пятом шаге функцииhwight64 (res = res + (res >> 16);) добавляется число, находящееся вследующей через одну за ней восьмерке; к последним двум восьмеркам неприбавляется ничего; при этом в предпоследней восьмерке будетзакодировано число, меньшее или равное 16, а в последней – меньшее илиравное 8.Условие о том, что в каждой восьмерке битов, кроме последней, в resзакодировано число, меньшее или равное 16, очевидно нужно, потому чтоздесь мы проверяем, что предыдущие операции прошли успешно.
Ведьочевидно, что в каждой восьмерке битов не может быть больше 8единичных битов, соответственно, сумма чисел в двух восьмерках будетменьше или равна 16 (кроме последней восьмерки). Аналогично – условиепро число в последней восьмерке.Рассмотрим утверждение для некотого i1 (в условии леммы для iстоит \forall).Из результата, полученного на четвертом шаге, создается bit_list (спомощью функции create_bit_list), из которого с помощью функцииread_num_from_bits считывается число, которое закодировано текущейвосьмеркой битов (начинающейся с индекса 8*i1).С другой стороны, из res (взятого до выполнения 5го шага) создаетсяbit_list (с помощью функции create_bit_list), с помощью функцииread_num_from_bits считывается число, которое закодировано этой жевосьмеркой битов (начинающейся с индекса 8*i1), к нему добавляется число,закодированное следующей через одну восьмеркой битов(начинающейся синдекса 8*i1+16).Две величины, полученные слева и справа, должны быть равны длявсех i от 0 до 5 (так как к последним двум 8кам мы ничего не добавляем),потому что на пятом шаге результат суммируется с тем же результатом,только сдвинутым на 16 (сложение первой четверти числа со второй, второйс третьей, третьей с четвертой).14Грубо говоря, данная лемма является условием, что мы правильнопонимаем, что именно происходит на пятом шаге.
В первой восьмерке мынакапливаем сумму единичных битов числа w. Заметим, что в памяти числозаписывается в обратном порядке, поэтому накопление идет в первойвосьмерке.Лемма num_ops_for_step6:@lemma num_ops_for_step6:@\forall unsigned long long res;@(((\forall integer i;@( (0 <= i < 6) ==>@read_num_from_bits(create_bit_list(res,BITS_PER_LONG), 8*i, 8) <= 32))@&&@( 16 >= read_num_from_bits(create_bit_list@(res, BITS_PER_LONG), 8*6, 8) )@&&@( 8 >= read_num_from_bits(create_bit_list@(res, BITS_PER_LONG), 8*7, 8) )@)@==>@((read_num_from_bits(create_bit_list((res + (res >> 32)), BITS_PER_LONG), 0, 8) ==@read_num_from_bits(create_bit_list@(res, BITS_PER_LONG), 0, 8) +@read_num_from_bits(create_bit_list@(res,BITS_PER_LONG), 32, 8) )@&&@( 8 >= read_num_from_bits(create_bit_list@((res + (res >> 32)), BITS_PER_LONG), 8*7, 8) ==@read_num_from_bits(create_bit_list@(res, BITS_PER_LONG), 8*7, 8) )@));@Здесь утверждается, что если в каждой восьмерке битов, кроме двухпоследних, в res закодировано число, меньшее или равное 32, впредпоследней восьмерке – меньшее или равное 16, а в последней –меньшее или равное 8, то к каждой восьмерке битов результата,полученного битовыми операциями на шестом (последнем) шаге функцииhwight64 (return (res + (res >> 32));) добавляется число, находящееся вчетвертой следующей за ней восьмерке; к последним четырем восьмеркамне прибавляется ничего; при этом в последней восьмерке закодированочисло, меньшее или равное 8.Условие о том, что в каждой восьмерке битов, кроме двух последних, вres закодировано число, меньшее или равное 32, очевидно нужно, потомучто здесь мы проверяем, что предыдущие операции прошли успешно.Очевидно, что в каждой восьмерке битов не может быть больше 815единичных битов, соответственно, сумма чисел в четырех восьмерках будетменьше или равна 32 (кроме последних двух восьмерок).
Аналогично –условие про число в последней восьмерке.Из результата, полученного на пятом шаге, создается bit_list (спомощью функции create_bit_list), из которого с помощью функцииread_num_from_bits считывается число, которое закодировано первойвосьмеркой битов.С другой стороны, из res (взятого до выполнения 6го шага) создаетсяbit_list (с помощью функции create_bit_list), с помощью функцииread_num_from_bits считывается число, которое закодировано этой жевосьмеркой битов, к нему добавляется число, закодированное четвертой,следующей за ней восьмеркой битов.Две величины, полученные слева и справа, должны быть равны,потому что здесь результат суммируется с тем же результатом, толькосдвинутым на 32 (сложение первой половины числа со второй), то есть кчислу, закодированному в первой восьмерке, прибавится число,закодированное в четвертой после нее восьмерке.Грубо говоря, данная лемма является условием, что мы правильнопонимаем, что именно происходит на шестом шаге.
В первой восьмерке мынакопили сумму единичных битов числа w. Это видно из порядка сложенийэтой восьмерки с остальными. То есть число, закодированное в этойвосьмерке, и есть число единичных битов в числе w, деле мы выделяем его спомощью маски 0x00000000000000FFull, отбрасывая остальные восьмерки.Количество и классификация сгенерированных леммДля bitmap_weight64:Всего: 51Условия корректности: 39Условия верификации: 10Условия завершимости: 2Для hweight64:Всего: 58Условия корректности: 40Условия верификации: 18Условия завершимости: 016Выводы, сделанные по результатам верификацииДопущения, при которых алгоритм является корректнымБыло сделано допущение, что корректность указателей на элементымассива означает отсутствие проблем с доступом к ним.Проблемы с инструментами верификации и предложения по ихулучшениюИнтерфейс редактора emacs при работе с pvs показался мненеудобным.Также, чтобы доказать некоторые леммы, их пришлось переносить в конецфайла .pvs, иначе не были видны аксиомы, необходимые для ихдоказательства.17ЗаключениеКоличество строк кода реализации: 603Из них строк спецификации в нотации ACSL: 544Количество тестовых вариантов: 4Количество доказанных лемм: 121 автоматически, 3 с помощью pvsВремя, затраченное на разработку тестов: 10 часовВремя, затраченное на доказательство корректности: 40 часовПоставленная задача решена полностью.
Для целевой функциидоказана корректность и проведено тестирование. Выявлена одна ошибкареализации.По результатам работы можно сделать вывод, что количествогенерируемых лемм растет примерно экспоненциально по мере ростаисходного кода. Решение подобных задач требует очень много временидаже для небольших алгоритмов.18.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
