Development and deductive verification of a predicate program of binary search, which is identical to bsearch.c program in the Linux kernel library, is described. New constructs in the predicate programming language for arbitrary types as program parameters are introduced. For an object of the arbitrary type, the transformation of coding an object via pointer is introduced.