Описывается построение и дедуктивная верификация предикатной программы бинарного поиска, идентичной программе bsearch на языке Си из библиотеки ОС Linux. В языке предикатного программирования определяются новые конструкции для произвольных типов в качестве параметров программ. Для объектов произвольного типа вводятся трансформации кодирования через указатели.