final-report-kiyko-2010 (1184395), страница 2
Текст из файла (страница 2)
Это аналог показателя точности работы алгоритма.predicate res_valid_recall(int *res, integer resSize, char *y, char*x, integer m, integer limit) =(\forall integer subpos;(0<=subpos<limit) && char_eq(y, x, subpos, m) ==>is_in_res(res, resSize, subpos));Предикат res_valid_recall описывает показатель полноту работы алгоритма. Для любой позиции встроке y, если с данной позиции начинается подстрока x, то она содержится в результате.Спецификация целевой функции HORSPOOL представлена ниже./*@ requires (0<=n) && (1<=m)@ && (\forall integer i1;@((0<=i1<n) ==> 0<=y[i1]<ASIZE))@ && (\forall integer i2;@((0<=i2<m) ==> 0<=x[i2]<ASIZE))@ && \valid_range(y, 0, n-1)@ && \valid_range(x, 0, m-1)@ && \valid_range(res, 0, n-1);@ ensures (\result >=0) &&@(res_valid_precision(res, \result, y, x, m)) &&@(res_valid_recall2(res, \result, y, x, m, n-m)) &&@no_repeats_grow(res, \result);@*/int HORSPOOL(const char *y,const char *x, int n,int m, int *res)Рассмотрим предусловия.1.
Длины строк корректны, удовлетворяют ограничениям и положительны.2. Строки x и y представляют массивы, размеры которых соответствуют указанным длинам.3. Элементы строк помещаются в выбранный алфафит 0..ASIZE.4. Указатель res ссылается на массив достаточного размера.Рассмотрим постусловия.1. res_valid_precision(res, \result, y, x, m).
Данная проверка идентична той, которая была впредыдущей спецификации.82. no_repeats_grow(res, \result). Осуществляется проверка более сильного условия, чем впредыдущей спецификации, а именно, условие возрастания элементов в результирующемсписке. Это условия удаѐтся автоматически доказать, в отличие от изначального условияотсутствия дубликатов, но, очевидно, что в возрастающем списке отсутствуют дубликаты.3. res_valid_recall(res, \result, y, x, m, n-m) проверяет для всех позиций в строке y, от 0 до n-m,наличие подстроки x длиной m символов.
Предыдущее условие было «для каждой позициине из результата, в y нет подстроки x. Теперь мы требуем «все подстроки отображены врезультате». Анализ показывает, что требования эквивалентны, но новое требование болеепрозрачно и легче специфицируется и доказывается пир помощи Frama-C.Дополнительно введѐнная функция memcmp1.Спецификация в предыдущей главе опиралась на существование и корректную работу встроеннойфункции memcmp, проверяющей две области памяти на равенство.На данном этапе работы потребовалось создание дополнительной функции вместо memcmp./*@ requires (size>=0) && \valid_range(a, 0, size-1) &&\valid_range(b,0,size-1);@ assigns \nothing;@ behavior eq:@ensures (\result == 0) ==> char_eq(a,b,0,size);@ behavior neq:@ensures (\result != 0) ==> char_neq(a,b,0,size);@*/int memcmp1(const char *a, const char *b, int size)Предусловия.1.
Переданные указатели указывают на доступную память.Постусловия.2. Результат не равен нулю, только если в данных строках есть отличающиеся элементы.Ошибки реализации алгоритмаОшибок в реализации алгоритма не было выявлено.Варианты и инвариантыВ функции memcmp1./*@ loop invariant (0<=i<=size) &&@char_eq(a,b,0,i);@ loop variant size-i;@*/for(i=0;i<size;i++) {if(a[i]!=b[i]) {return 1;}}Инвариант.1. До текущей позиции строки совпадают.2.
Счѐтчик i находится в пределах от 0 до size и следовательно, обращение к a и b по данномуиндексу корректно.9Вариант.1. Size – i всегда положительно и уменьшается в каждой итерации.В целевой функции HORSPOOL./*@ loop invariant (0 <= a <= ASIZE) &&@ \forall integer i2;@ (0<=i2<a) ==> bm_bc[i2] == m;@ loop variant ASIZE-a;@*/for (a = 0; a < ASIZE; a++)bm_bc[a] = m;Всем элементам bm_bc присваивается значение m. Инвариант: все элементы до текущего “a”равны m.
Вариант: ASIZE-a./*@ loop invariant (m>=1) && (0<= j <= m-1) &&@ (bm_bc_valid_generation(bm_bc, x, m, j));@ loop variant m-1-j;@*/for (j = 0; j < m - 1; j++)Инвариант: специальный предикат проверяет, что до j-го символа x массив сгенерированправильно, а так же то, что счѐтчик не выходит за допустимые пределы. Вариант: значение m-1-jположительно и уменьшается в каждой итерации.Основной цикл./*@ loop invariant (0<=i<=n) && (0<= resSize <= n) && (i>=resSize) &&@(res_valid_precision(res, resSize, y, x, m)) &&@(res_valid_recall(res, resSize, y, x, m, i)) &&@(resSize==0 || res[resSize-1]<i) &&@no_repeats_grow(res, resSize);@ loop variant n-m-i;@*/Инварианты.
Счѐтчик i не выходит за пределы строки и resSize не выходит за допустимыепределы. Условия точности и полноты работы алгоритма выполняются таким образом, чтопроверка осуществляется до текущей позиции i. Таким образом, в крайнем значении счѐтчика,инвариант обращается в постусловие.Сгенерированные леммыТип леммыусловиякорректностиусловияверификацииусловиязавершимостиКоличество31 лемма (HORSPOOL), 10 лемм (memcmp1) (корректность обращения куказателью, корректность вызова memcmp1, переполнение в арифметическихоперациях)49 лемм, относящихся к HORSPOOL, 12 лемм, относящихся к memcmp1(инварианты цикла, выполнение инвариантов цикла до 1-й итерации,постусловия)10 лемм (HORSPOOL), 2 леммы (memcmp1) (варианты циклов)10ВыводыАлгоритм является корректным при условии, что в качестве параметров ему передаются двестроки, символы которых принадлежат алфавиту.
Других допущений не требуется.Проблемы с инструментами.1. Свойства типа assigns. Описание простого свойства assigns вызывает ошибку компиляции.В связи с тем, что в задании assigns специфицировать необязательно, решать эту проблемуне пришлось.2. Автоматические пруверы иногда повисают, прекращают свою работу и т.д. К счастью,обычно проблема решается перезапуском прувера.11ЗаключениеКоличественные характеристики работыВеличинаКоличество строк кода реализацииКоличество строк спецификации внотации ACSLКоличество тестовых вариантовКоличество доказанных леммВремя, затраченное на разработку тестов(1 этап)Время, затраченное на доказательствокорректностиЗначение в соответствующих ед. изм.30 строк417 строк10215 всего, вручную 01,5 рабочих дня6-7 рабочих днейВывод:В результате работы было формально доказано то, что при корректных входных параметрахалгоритм всегда завершается и результат его работы удовлетворяет требованиям, следующим изего функционального назначения.
Иными словами, алгоритм корректно находит все подстроки.12.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
