Deductive verification and optimization of the predicate program for string concatenation

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.