Formal approach to program verification

Abstract

Program verification has played an important role in today's production of reliable software [3]. The most popular method of verification is given by Hoare. Other mathematicians and programmers also offered their method based on Hoare's principles. This thesis proposes a different approach to program verification using Hoare notation. In this thesis, we introduced a new method based on Hoare triple and some inference rules as a tool for program correctness proof. The proposed approach adopted conventional black-box and white-box tests [6] to carried out a systematic and rigorous program verification.