final-report-chernikova-2011 (1184399), страница 2

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

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

Аналогично для перестановки: из легких длядоказательства свойств сохранения одних элементов массива и сдвига другихследует более сложное. Вариант цикла опять же очевиден.Инварианты и вариант для цикла вставки первого элемента на нужное место:/*@loop invariant 1<=j<=size;for permutation: loop invariant eq_arr{Here, E}(a,j,size-1) &&moved_back_array{Here, E}(a, 0, j-1) && permutation{E, Pre}(a, 1,size-1);for sorted: loop invariant sorted(a,size) && (\forall integer p;(0<p<j ==> a[p]<backup));loop variant size-j;*/Опять же для перестановки условия сохранения в итерации одних элементовмассива и сдвига других, для упорядоченности – сама упорядоченность иусловие цикла. Вариант очевиден – счетчик увеличивается в каждой итерациина 1.83.4.

Количество и классификация сгенерированных леммУсловия:• корректности – 38 (1 для setMin)• верификации – 53(2 для setMin, 3 из тех, что для основной функции, доказанывручную)• завершимости – 6 (варианты циклов)8 лемм для предикатов записаны самостоятельно, из них 1 доказана вручную.3.5. Выводы, сделанные по результатам верификацииНикаких допущений, обеспечивающих корректность алгоритма, приверификации сделано не было.Проблемы с инструментами верификации и предложения по их улучшению:Автоматический прувер не во всех случаях справился со сложным предикатом,заданным через аксиомы.

Также были выявлены некоторые ошибки прииспользовании assert.9······ЗаключениеКоличество строк кода реализации: 20Количество строк спецификации в нотации ACSL: 96Количество тестовых вариантов: 4Количество доказанных лемм: 105, из них 4 вручную с помощью PVSВремя, затраченное на разработку тестов: 4 часаВремя, затраченное на доказательство корректности: 60 часов (из них 12на доказательство лемм вручную с использованием PVS)Поставленная задача решена полностью. Для данной функции доказанакорректность. По результатам работы можно сделать вывод, что данный подходк верификации (второй этап работы) требует достаточно много времени и силдаже для такого небольшого алгоритма, следовательно не слишком удобен виспользовании и для сложных алгоритмов.10.

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

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