The programming language P defines a class of programs which do not interact with the external environment. Infinite execution of such programs is meaningless, so the execution of a correct P program must terminate. Loops and pointers are prohibited in the P language. In present article the method of deductive verification for predicate programs is developed. The formula of total correctness for a predicate program with respect to its specification using the formal operation semantics is presented. The rules of decomposition the total correctness formula into simple and short formulas are developed. The correctness of rules is proved in PVS. A tool for deductive verification that generates formulas of program correctness is implemented. The correctness formulas are generated by using the system of rules. The correctness formulas are then translated to the SMT-solver CVC3 and the specification language of PVS-system. The type compatibility errors can lead to an unpredictable behavior of a program. The translator of P language performs full type checking. Some checks couldnt be discharged statically. They are translated to the PVS specification language for use to prove it in the PVS. All correctness formulas are first tested in the SMT-solver CVC3. Unsolved formulas are then translated to the set of theories in the PVS specification language.