final-report-kononov-2010 (1184392), страница 2

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

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

В тот момент, когдапеременная l примет значение большее, чем 1, при вычислении значения переменной m произойдёт переполнение.Для устранения данной ошибки, был предложен следующий вариант получения значения переменной m:int m = l + (h - l)/2.3.3 Описание выбранных инвариантов и вариантовloop invariant 0 <= l && h <= nmemb - 1 &&\forall integer i; 0 <= i < nmemb && base[i] == key ==> l <= i <= h;loop variant h-l;Инвариант означает, что если в массиве есть элементы, равные объекту, который необходимонайти, то индексы этих элементов лежат в диапазоне, задаваемом переменными l и h.Вариантом цикла является размер диапазона индексов, среди которых ведётся поиск объектаkey.3.4 Количество и классификация сгенерированных леммВсего: 34.Условия корректности: 15.Условия завершимости: 4.7Условия верификации: 15.3.5 Выводы, сделанные по результатам верификацииАлгоритм является корректным, если ему будут переданы параметры, удовлетворяющие требованиям, описанными в пункте 3.1.

Также необходимо заменить выражение подсчёта значения середины диапазона выражением, в котором не будет возникать ситуаций с переполнением, например,выражением, предложенным в пункте 3.3.84. ЗаключениеКоличество строк кода реализации: 23.Количество строк спецификации в нотации ACSL: 14.Количество тестовых вариантов: 4.Количество доказанных лемм: 34 автоматически.Общее затраченное время: 40.Поставленная задача решена полностью. На этапе верификации алгоритма обнаружена ошибка ипредложен вариант её исправления.В связи с тем, что предложенный для тестирования алгоритм имеет простой граф потока управления, то использование каких бы то ни было полуавтоматических средств для его верификации, намой взгляд, является не оправданной тратой времени.9.

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

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