final-report-kuzin-2010 (1184396), страница 3
Текст из файла (страница 3)
list_length(i->i_klist, next) считает расстояние от второго элемента до головысписка, всегда положительно и уменьшается в каждой итерации.16Количество и классификация сгенерированных леммТип леммыУсловиякорректностиКоличествоKnode_dead – 1 леммаKlist_release - 5 леммKlist_dec_and_del – 4 леммыKlist_iter_init_node – 6 леммKlist_iter_init - 1 леммаKlist_put – 2 леммыKlist_iter_exit – 5 леммKlist_next - 27 лемм (доказывается 25 в связи с тем что возможнопереполнение)(корректность обращения к указателю, переполнение в арифметическихоперациях)УсловияверификацииKnode_dead – 1 леммаKlist_release - 1 леммаKlist_dec_and_del – 3 леммыKlist_iter_init_node - 6 леммKlist_iter_init - 1 леммаKlist_iter_exit – 4 леммыKlist_next - 80 лемм(инварианты цикла, выполнение инвариантов цикла до 1-й итерации,постусловия)Условиязавершимостиklist_next - 4 леммывариант циклаВыводыПри верификации были сделаны следующие допущения:1.
При удалении элемента из списка, полям next и prev данного элемента присваиваетсяуказатель на этот элемент.2. Упрощен вид списка.3. Все указатели имеют один и тот же базовый адрес.Проблемы с инструментами.Возникли проблемы при работе с указателями которые плохо поддаются формализациина ACSL. Так же, не доказываются автоматически утверждения вида a ==> b при условии,что утверждение c доказано, и существует лемма a && c ==> b. Решением даннойпроблемы стала модификация исходных утверждений. Кроме того, Jessie неподдерживает приведение указателей. Решением данной проблемы стало существенноеупрощение типов, используемых в функциях.17Заключение-Количество строк кода реализации: 334Количество строк спецификации в нотации ACSL: 158Количество тестовых вариантов: 7 состояний, 220 переходовКоличество доказанных лемм: 148 автоматически, 3 не доказано в связи сошибками в функцияхВремя затраченное на разработку тестов: 23 часаВремя затраченное на доказательство корректности: 50 часовВывод:В результате работы было формально доказано то, что при корректных входныхпараметрах алгоритм всегда завершается и результат его работы удовлетворяеттребованиям, следующим из его функционального назначения.
Кроме того было найденонесколько ошибок в функциях (неверное условие, теоретическая возможностьпереполнения).18.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
