final-report-khairulin-2010 (1184394), страница 2

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

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

Исходя из логики работы алгоритма, скачок может составить |pattern|символов. Таким образом, может произойти переполнение переменной типа int. Поэтомумаксимальная длина строки составляет MAX_INT / 2.3.4.2 Проблемы с инструментами верификации и предложения по ихулучшению7Проблемы:1. Нумерация лемм. Если доказать какие-то леммы (инварианты), а потомвернуться к исходному файлу и добавить еще несколько инвариантов в этуфункцию, то номера лемм смещаются, и приходится вручную править файл*.prf.2.

Имена переменных. Если доказать какие-то леммы (инварианты), а потомдобавить глобальные леммы, то могут измениться имена переменных(например alloc-таблиц). В связи с чем старые доказательства, использующиеinst перестанут работать.Пожелания по улучшению:1. Добавить в gWhy отображение доказательств, доказанных вручную2. Добавить в PVS какую-нибудь возможность работы с переменными и ихподстановками. На данный момент очень неудобно применять леммы, т.к. приподстановке переменных приходится открывать отдельный файл, в которомкопипастом выписывать нужные параметры.84. ЗаключениеКоличество строк кода реализации: 308Количество строк спецификации в нотации ACSL: 130Количество тестовых вариантов: 6Количество доказанных лемм 337 (327 автоматически, 10 вручную с помощью PVS)Время, затраченное на разработку тестов: 1 часВремя, затраченное на доказательство корректности: 100-120 часов (Из них часов 30 – надоказательство вручную 10 лемм с использованием PVS)Поставленная задача решена полностью.

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

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

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