final-report-rogozhkin-2010 (1184400), страница 2
Текст из файла (страница 2)
Так как первый символ гарантированно не равен нулю, то это означает, что в самомплохом случае равна 1.lemma strlen_comp:\forall char* s1, char* s2;((s1 == s2 + 1) && (*s != 0)) ==> (strlen(s2) > strlen(s1));Эта лемма говорит о том, что длина строки, которая ссылается на следующий символ исходнойстроки, всегда меньше длины исходной строки, если исходная строка не начинается с нулевогосимвола.Спецификация целевой функции strtok_r представлена ниже.requires (((s1 != NULL && \valid(s1) && \valid_range(s1,0,strlen(s1)))|| ((s1==NULL) && (*lasts==NULL))|| ((s1==NULL) && (*lasts != NULL) && \valid(*lasts) &&\valid_range(*lasts,0,strlen(*lasts))))&& (\valid_range(s2,0, strlen(s2)))&& (\valid(lasts)));behavior empty:assumes ( (s1==NULL) && (*lasts==NULL) );ensures ( (\result==NULL)&& (*lasts == NULL));behavior no_sepps_s1:assumes ( (s1 != NULL) && !str_contain_chars(s1, s2) );ensures ( (\old(s1) != NULL) && (char_eq(\result, \old(s1)) &&(*lasts == NULL)) );behavior no_sepps_lasts:assumes ( (*lasts != NULL) && (s1 == NULL) && !str_contain_chars(*lasts, s2) );ensures ( (\old(*lasts) != NULL) && (s1 == NULL) && char_eq(\result,\old(*lasts)) && (*lasts == NULL));behavior seppse_everywhere_s1:assumes ( (s1 != NULL) && str_contain_only_chars(s1,s2) );ensures ( (\old(s1) != NULL) && (\result == NULL) && (*lasts ==NULL) );behavior seppse_everywhere_lasts:assumes ( (*lasts != NULL) && (s1 == NULL) &&str_contain_only_chars(*lasts,s2) );ensures ( (\old(*lasts) != NULL) && (s1 == NULL) && (\result ==NULL) && (*lasts == NULL) );behavior sepps_where_they_want_s1:assumes ( (s1 != NULL) && !str_contain_only_chars(s1,s2) );ensures ( char_eq_l(\old(s1)+firstSeppsLength(\old(s1),s2,0),\result, strlen(\result))&& (str_contain_char(s2, \old(s1)[strlen(\result) +firstSeppsLength(\old(s1),s2,0)]) ||(strlen(\result) + firstSeppsLength(\old(s1),s2,0) ==strlen(\old(s1))))&& !str_contain_chars(\result, s2)&& ( ( (strlen(*lasts) == strlen(\old(s1))-strlen(\result)-1firstSeppsLength(\old(s1),s2,0)) &&char_eq_l(\old(s1)+firstSeppsLength(\old(s1),s2,0)+strlen(\result)+1, *lasts, strlen(*lasts)))|| (*lasts == NULL)));behavior sepps_where_they_want_lasts:assumes ( (*lasts != NULL) && (s1 == NULL) && !str_contain_only_chars(*lasts,s2) );ensures ( char_eq_l(\old(*lasts)+firstSeppsLength(\old(*lasts),s2,0), \result, strlen(\result))&& (str_contain_char(s2, \old(*lasts)[strlen(\result) +firstSeppsLength(\old(*lasts),s2,0)]) ||(strlen(\result) + firstSeppsLength(\old(*lasts),s2,0) ==strlen(\old(*lasts))))&& !str_contain_chars(\result, s2)&& ( ( (strlen(*lasts) == strlen(\old(*lasts))-strlen(\result)-1firstSeppsLength(\old(*lasts),s2,0)) &&char_eq_l(\old(*lasts)+firstSeppsLength(\old(*lasts),s2,0)+strlen(\result)+1, *lasts,strlen(*lasts)))|| (*lasts == NULL)));char* strtok_r(char *s1, const char *s2, char **lasts)Рассмотрим предусловия.1.
Корректный указатель s22. Корректный указатель lastsNULL3. Либо s1 и *lasts равны NULL, либо s1 не равен NULL, либо s1 равен NULL и *lasts не равенРассмотрим постусловия. Все предусловия делятся на несколько поведений.1. emptyДанное поведение проверяет результат на NULL, если s1 и *lasts равны NULL2. no_sepps_s1, no_sepps_lastsОба эти поведения требуют, что строка не содержала разделителей и проверяют, равен ли токенисходной строки и равен ли lasts NULL.3. seppse_everywhere_lasts, seppse_everywhere_s1 проверяют равны ли результат и lasts NULL,при условии, что строка полностью состоит из разделителей4.
sepps_where_they_want_s1, sepps_where_they_want_lasts проверяют равны ли длинаисходной строки сумме длин удалённых разделителей, результата и lasts, содержится ли в исходнойна правильном месте токен, является ли следующий за токеном символ разделителем, корректныйли остаток строки записан в lasts при условии, что в строке содержатся разделители.Ошибки реализации алгоритмаОшибок в реализации алгоритма не было выявлено.Варианты и инварианты/*@ loop invariant (\valid(s1) && str_contain_chars_l(start, s2, s1-start));@ loop variant (strlen(s1)+1);@*/for( ; (c = *s1) != 0; s1++ )Инвариант.1.
До текущей позиции строки все символы - разделители2. s1 корректный указательВариант.1. Длина строки уменьшается и всегда сумма длины строки и единицы больше нуля/*@ loop invariant \valid(sepp);@ loop variant (strlen(sepp)+1);@*/for( sepp = s2 ; (sc = *sepp) != 0 ; sepp++ ) {Инвариант.1. sepp корректный указательВариант.1. Длина строки уменьшается и всегда сумма длины строки и единицы больше нуля/*@ loop invariant \valid(s1) && !str_contain_chars_l(\at(s1,Pre), s2, s1-\at(s1,Pre));@loop variant (strlen(s1)+1);@*/for( ; (c = *s1) != 0; s1++ )Инвариант.1.
До текущей позиции строки нет разделителей2. s1 корректный указательВариант.1. Длина строки уменьшается и всегда сумма длины строки и единицы больше нуля/*@ loop invariant \valid(sepp) && !str_contain_char_l(\at(s2,Pre), c, \at(s2,Pre)-s2);@loop variant (strlen(sepp)+1);@*/for( sepp = s2; (sc = *sepp) != 0; sepp++ )Инвариант.1. До текущей позиции строки в строке не встречается символ с2.
sepp корректный указательВариант.1. Длина строки уменьшается и всегда сумма длины строки и единицы больше нуляОбоснование корректности недоказанных леммBehavior sepps_where_they_want_lastsЛемма № 9. AssertionУтверждение: assert (strlen(tok) + firstSeppsLength(start,s2,0) == strlen(start));Корректность: Эта лемма корректна, т.к. если алгоритм достиг оператора рядом с этим ассертом,то разделители могли встречаться только вначале строки. Значит длина токена + длина разделителейвначале = длина исходной строки.Behavior DeffaultЛемма № 7.
AssertionУтверждение: assertion(true);Корректность: Лемма возникает из-за аанотации breaks(c == sc). И не может доказать, что извнутреннего цикла при c == sc происходит выход. Мне кажется, эта баг инструмента. Возможно онпутает аннотации к внутреннему и внешнему циклу. Если убрать breaks аннотацию у внутреннегоцикла,то леммы не возникнет. Так же если убрать аннотацию breaks и вместо неё добавить в условиеif аннотацию assert (c == sc), то лемма автоматически докажется.Лемма № 9. invariant preservedУтверждение: loop invariant \valid(sepp);Корректность: Указатель на sepp всегде корректен, т.к. в любой итерации цикла он равен суммеуказателя на s2 инекоторого положительного числа, которое меньше длины строки s2Лемма № 10. AssertionУтверждение: assert !str_contain_char(s2,*s1) || (*s1 == 0);Корректность: Ассерт корректен, т.к.
следуя логике кода, алгоритм может выйти из цикла либо еслитекущий символ s1 не разделитель,либо текущий символ s1 равен символу конца строки, т.е. строка s1 закончиласьЛемма № 11. AssertionУтверждение: assert ((start != s1) ==> str_contain_chars(start, s2));Корректность: Ассерт корректен, т.к. если s1 не равен start, то значит из s1 сдвинулся из-за удалениясимволов разделителей, значит startточно содержит символы разделителиЛемма № 16. AssertionУтверждение: assert s1 == start+firstSeppsLength(start,s2,0);Корректность: Ассерт корректен, т.к. если указатель на s1 всегда равен сумме указателя на start иколичеству удалённых символов разделителей.Лемма № 17. AssertionУтверждение: !str_contain_only_chars(start,s2);Корректность: Исходная строка не состоит полностью из разделителей, т.к.
этот случай был обработанс помощью if выше по коду.Лемма № 22. invariant preservedУтверждение: loop invariant \valid(s1);Корректность: Указатель на s1 всегде корректен, т.к. в любой итерации цикла он равен суммеуказателя на start инекоторого положительного числа, которое меньше длины строки startЛемма № 23. invariant preservedУтверждение: loop invariant !str_contain_chars_l(\at(s1,Pre), s2, s1-\at(s1,Pre);Корректность: До текущего символа s1 не содержит разделителей, т.к.
если бы один из символов былбы разделителем, функция завершила бы свою работуиз-за истинности внутреннего условия.Лемма № 26. invariant preservedУтверждение: loop invariant !str_contain_char_l(\at(s2,Pre), c, \at(s2,Pre)-s2);Корректность: До текущего символа s2 не содержит с, т.к.
если бы с был равен одному изпредыдущих символов, функция завершила бы свою работуиз-за истинности внутреннего условия.Лемма № 36. AssertionУтверждение: assert !str_contain_chars(tok, s2);Корректность: Токен не содержит символов разделителей, т.к. перед последним циклом он былравен указателю на s1. А указатель на s1 мого достигнуть этого когда, только если полностьюзавершился цикл. Т.е. если в нём не было ни одного разделителя.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
