Для верификации функции мы должны определить ее назначение с помощью двух утверждений. Предусловие определяет состояние, в котором должна находиться программа в момент вызова функции, а постусловием называется то, что будет гарантироваться функцией при ее завершении. Таким образом мы можем определить функцию двоичного поиска на языке С следующим образом:
int bsearch(int t. int x[], int n)
/* precondition x[0] <= x[l] <= <= x[n-l]
postcondition
result == -1 => t not present in x
0 <= result < n => x[result] == t*/
Эти условия представляют собой скорее соглашения, нежели факты. В них утверждается, что если выполнены предусловия, то выполнение функции приведет к истинности постусловий. После того как будет доказано то, что тело функции обладает этим свойством, соотношением между пред- и постусловиями можно будет пользоваться без углубления в подробности реализации. Этот подход к написанию программного обеспечения называется «программированием по контракту».
Опубликовал vovan666
April 16 2013 23:58:13 ·
0 Комментариев ·
3099 Прочтений ·
• Не нашли ответ на свой вопрос? Тогда задайте вопрос в комментариях или на форуме! •
Комментарии
Нет комментариев.
Добавить комментарий
Рейтинги
Рейтинг доступен только для пользователей.
Пожалуйста, залогиньтесь или зарегистрируйтесь для голосования.
Нет данных для оценки.
Гость
Вы не зарегистрированны? Нажмите здесь для регистрации.
Главная
Каталог файлов
