PROGRAMMING LOGIC AND PROGRAM CORRECTNESS PROOF
Yong Feng · Chinese Journal of Computers · 1983
This paper is a continuation of [2]. First, an extended natural deduction system of the programming logic is established and then its completeness is proved. Second, a number of theorems in this formal system are obtained and their application to reasoning about program correctness is demonstrated with some examples.