Abstract: This paper expounds the basic theory and basic ideas of Formal derivation method of programs. Formal devivation of programs is a developing method of programs based on the proof theory of program correctness. It can make the proof process and the devolopment of the program in progress in the meantime. And this paper illustrates how to use formal derivation of programs.

Key words: formal derivation method of programs, program specification, loop invariant, boundary function