final-report-kononov-2010 (решения 2010 года), страница 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.