Deductive verification is simplier and faster to perform for the predicate programs then for the analogous imperative program. For each C program, it is possible to construct an equivalent predicate program and optimize it so that resulting program coincides the source C program. This method is illustrated for the C library function strcat. The construction, deductive verification, and optimizing transformation of the predicate program strcat is described. New method of string coding via two pointers has been developed.