Axiomatic Basis for Computer Programming
Lauretta Oluwafemi Osho, Francisca Nonyelum Ogwueleka, Oluwafemi Osho · Universal Journal of Computational Mathematics · 2013
This paper considers a formal method, known as axiomatic semantics, used to prove the correctness of a computer program. This formal method extracts, using some proof rules, the mathematical verification conditions from a computer program. The axioms of program flow, including, sequential flow, iteration, and alternation flows are presented. Using the axiomatic basis the completeness of two variants of integer multiplication program is proved. Results show that computer programs can actually be verified sufficiently for correctness without necessarily testing them, or more practically put, to complement their testing.