The authors present an axiomatic approach which enables one to prove by formal methods that his program is totally correct (i.e., it terminates and is logically correct -- does what it is supposed to do). The approach is similar to Hoare's approach for proving that a program is partially correct (i. e., that whenever it terminates it produces correct results). The extension to Hoare's method lies in the possibility of proving correctness and termination at once, and in the enlarged scope of properties that can be proved by it.