final-report-rogozhkin-2010 (1184400), страница 3

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

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

Соответсвенно токен тоже несодержит разделителей.Лемма № 38. invariant preservedУтверждение: loop invariant \valid(s1);Корректность: лемма №22Лемма № 39. invariant preservedУтверждение: loop invariant str_contain_chars_l(start, s2, s1-start);Корректность: До текущего символа s1 содержит только разделители, т.к. если бы один из символовне был бы разделителем, функция вышла бы из цикла из-за истинности внутреннего условия.Лемма № 41.

AssertionУтверждение: assert ((start != s1) ==> str_contain_chars(start, s2));Корректность: лемма №11Лемма № 42. AssertionУтверждение: assert str_contain_only_chars(start,s2);Корректность: Если символ с равен нулю, значит достигнут конец исходной строки, соответственновсе символы исходной строки - разделители.Лемма № 43. AssertionУтверждение: assert str_contain_chars(start, s2);Корректность: лемма №42Лемма № 72. AssertionУтверждение: assertion(true);Корректность: лемма №7Лемма № 74. invariant preservedУтверждение: loop invariant \valid(sepp);Корректность: лемма №9Лемма № 75. AssertionУтверждение: assert !str_contain_char(s2,*s1) || (*s1 == 0);Корректность: лемма №10Лемма № 76.

AssertionУтверждение: assert ((start != s1) ==> str_contain_chars(start, s2));Корректность: лемма №11Лемма № 81. AssertionУтверждение: assert s1 == start+firstSeppsLength(start,s2,0);Корректность: лемма №16Лемма № 82. AssertionУтверждение: !str_contain_only_chars(start,s2);Корректность: лемма №17Лемма № 87. invariant preservedУтверждение: loop invariant \valid(s1);Корректность: лемма №22Лемма № 88.

invariant preservedУтверждение: loop invariant loop invariant !str_contain_chars_l(\at(s1,Pre), s2, s1-\at(s1,Pre);Корректность: лемма №23Лемма № 91. invariant preservedУтверждение: loop invariant !str_contain_char_l(\at(s2,Pre), c, \at(s2,Pre)-s2);Корректность: лемма №26Лемма № 101. AssertionУтверждение: assert !str_contain_chars(tok, s2);Корректность: лемма №31Лемма № 103. invariant preservedУтверждение: loop invariant \valid(s1);Корректность: лемма №22Лемма № 104. invariant preservedУтверждение: loop invariant str_contain_chars_l(start, s2, s1-start);Корректность: лемма №39Лемма № 106.

AssertionУтверждение: assert ((start != s1) ==> str_contain_chars(start, s2));Корректность: лемма №11Лемма № 107. AssertionУтверждение: assert str_contain_only_chars(start,s2);Корректность: лемма №42Лемма № 108. AssertionУтверждение: assert str_contain_chars(start, s2);Корректность: лемма №43Сгенерированные леммыТип леммыусловия корректностиусловия верификацииусловия завершимостиВыводыКоличество54 леммы (корректность обращения к указателю,переполнение в арифметических операциях)231 лемма (инварианты цикла, выполнениеинвариантов цикла до 1-й итерации, постусловия)22 леммы (варианты циклов)Алгоритм является корректным при условии, что в качестве второго параметра ему передаетсяуказатель, который не ссылается на NULL.

Других допущений не требуется.Проблемы с инструментами.1. Свойства типа assigns. Описание простого свойства assigns вызывает ошибку компиляции. Всвязи с тем, что в задании assigns специфицировать необязательно, решать эту проблему непришлось.2. Автоматические пруверы иногда повисают, прекращают свою работу и т.д. К счастью,обычно проблема решается перезапуском прувера.ЗаключениеКоличественные характеристики работыВеличинаКоличество строк кода реализацииКоличество строк спецификации в нотации ACSLКоличество тестовых вариантовКоличество доказанных леммВремя, затраченное на разработку тестов (1 этап)Время, затраченное на доказательствокорректностиЗначение в соответствующих ед.

изм.5017773542 рабочих дня4-5 рабочих днейВывод:Поставленная задача решена не полностью. Для функции strtok проведенотестирование. Корректность функции доказана не полностью. Верифицирована значительнаячасть исходного кода функции.В результате работы было формально доказано то, что при некоторых корректныхвходных параметрах алгоритм всегда завершается и результат его работы удовлетворяеттребованиям, следующим из его функционального назначения..

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

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