формальное доказательство алгоритмов поиска

[Dilu]

Уважаемые знатоки, пожалуйста, помогите. Пишу диплом, по дисциплине "Математические основы информатики". Обучение по книге Гриса "Наука программирования". Написал почти все, не выходит составить алгоритм для бинарного поиска. Если кто знает, напишите пред-, постусловие и инвариант. Пожалуйста, уже нет сил...помогите...

[Dilu]

никто не знает? Люди, выручайте:(

[Sonic86]

Так, я не понял! Я щас напишу - посмотрите - то или нет.
Пусть $M$ - отсортированный по возрастанию массив из элементов, содержащий элемент $a$ (т.е. $(\exists j)M[j]=a$). Надо найти номер этого элемента (т.е. $j$) Делается так: массив $M$ делится на 2 части $M_1, M_2$, берется серединный элемент $b$, если $b>a$, то ищем элемент в массиве $M_1$, иначе - в массиве $M_2$. Вот такой поиск называется двоичным, а запрограммировать его (что несложно) - это и есть Ваша задача