final-report-akovalenko-2011 (1184397), страница 2

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 2)

Во второй – доказываем правильность работыфункции в целом и на каждом этапе.3.2. Описание ошибок в реализации, которые были выявлены припомощи верификацииВ ходе верификации ошибок в реализации обнаружено не было.3.3. Инварианты и варианты//@ ghost int coord_old = -1;/*@ loop invariant 0 <= num_frames_left <= set->num_frames@&& 0 <= (set->num_frames - num_frames_left)< MAX_FRAMES_ON_STACK@&&coord==num_frames_left) * NUM_SLOTS_PER_FRAME(set->num_frames-14@&& 0 <= k <= coord@&& (coord == coord_old + 1)@- num_frames_left)&& frame == set->frames + (set->num_frames@num_frames_left)&& get_frame(coord) == (set->num_frames -@&& get_slot(coord) == 0@<= coord)&& (\forall integer r; (0 <= r < k) ==> res[r]@>frames[get_frame(res[q])]get_slot(res[q]) - 1))) != 0)&& (\forall integer q; (0 <= q < k) ==> (set& (1 << (NUM_SLOTS_PER_FRAME -@&& (\forall integer j; ((0 <= j < coord) &&(\forall integer w; (0 <= w < k) ==> (res[w] != j))) ==> (set>frames[get_frame(j)] & (1 << (NUM_SLOTS_PER_FRAME - get_slot(j) 1))) == 0)@;@ loop variant num_frames_left;@*/coord_old – для доказательства факта, что на каждом шаге цикла coordувеличивается на единичку.Далее следуют инварианты вытекающие из преусловий функции,инварианты на coord (текущая координата просматриваемого слота висходном множестве) и операций с coord, проверка постусловия самойфункции для каждой итерации цикла.Вариантом цикла выбрана переменная num_frames_left, которая накаждом шаге цикла уменьшается на 1.15/*@@ loop invariant 0 <= i <= NUM_SLOTS_PER_FRAME@&&0<=num_frames_left) < MAX_FRAMES_ON_STACK(set->num_frames@&& 0 <= k <= coord@&& (coord == coord_old + 1)-@&& frame == set->frames + (set>num_frames - num_frames_left - 1)@&&>num_frames - num_frames_left - 1)get_frame(coord)get_slot(coord)==(set-@(NUM_SLOTS_PER_FRAME - i)&&==@res[r] <= coord)&& (\forall integer r; (0 <= r < k) ==>@&& (\forall integer q; (0 <= q < k) ==>(set->frames[get_frame(res[q])] & (1 << (NUM_SLOTS_PER_FRAME get_slot(res[q]) - 1))) != 0)@&& (\forall integer j; ((0 <= j < coord)&& (\forall integer w; (0 <= w < k) ==> (res[w] != j))) ==> (set>frames[get_frame(j)] & (1 << (NUM_SLOTS_PER_FRAME - get_slot(j) 1))) == 0)@;@ loop variant i;@*/Инварианты, вытекающие из преусловий функции и цикла,инварианты на coord и операции с coord, проверка постусловия самойфункции для каждой итерации цикла.16В качестве варианта для цикла выбрана переменная i, котораяуменьшается на каждом шаге на 1.3.4.

Количество и классификация сгенерированных леммУсловия:•корректности - 23•верификации - 67•завершимости – 63.5. Выводы, сделанные по результатам верификацииДопущения, при которых алгоритм является корректным:•ограничение по количеству слотов в исходном множестве;• не проверяем, выделена ли память под массив координат res.Проблемы с инструментами верификации и предложения по ихулучшению:•если все леммы не доказываются автоматически полностью, товозникает проблемы с доказательством битового сдвига.

Былаподключена#pragmaJessieIntegerModel(math),нонедоказывались все инварианты (как впоследствии оказалось, нехватало данных) и не доказывался битовый сдвиг – прувер немог доказать, что \forall int i; (0 <= i < 8) ==> 1 <= (1 << i) <= 128(не доказывалась лемма, что 1 <= asr(2147483647, i_4_1)). Кактолько были подправлены инварианты, всё, включая битовыйсдвиг, доказалось автоматически прувером Alt-Ergo.

ПруверCVC3 эту лемму доказать так и не смог. Сложно предложитьздесь решение проблемы, не зная, почему такая проблема17возникает. Мне кажется, что это просто некоторый баг – ведьинварианты ссылались на этот битовый сдвиг, а не наоборот.184. ЗаключениеКоличество строк кода реализации: 115Количество строк спецификации в нотации ACSL: 68Количество тестовых вариантов: много (попытки вызвать ошибки ввыделении памяти)Количество доказанных лемм 96 (автоматически)Время, затраченное на разработку тестов: 1 час + 1 час (послевведения ветвей функциональности)Время, затраченное на доказательство корректности: 50-60 часов (изних часов 15 – на попытки доказательства вручную некоторых лемм сиспользованием PVS)Поставленная задача решена полностью.

Для предлагаемой функцийдоказана корректность.По результатам работы можно сделать вывод, что данный подходявляется очень сложным и не всегда понятным (особенно на втором этапе).Требует очень много времени и сил даже для небольших алгоритмов.19.

Характеристики

Список файлов учебной работы