Universal Journal of Computational Mathematics(CEASE PUBLICATION) Vol. 1(3), pp. 67 - 72
DOI: 10.13189/ujcmj.2013.010301
Reprint (PDF) (367Kb)

Axiomatic Basis for Computer Programming

Lauretta O. Osho¹, Francisca Ogwueleka², Oluwafemi Osho^3,*
1 Department of Computer Science, Federal University of Technology, Minna, Nigeria
² Department of Computer Science, Federal University, Wukari, Nigeria
³ Department of Cyber Security Science, Federal University of Technology, Minna, Nigeria

ABSTRACT

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.

KEYWORDS
Computer, Computer Programming, Axiomatic, Completeness, Correctness

Cite This Paper in IEEE or APA Citation Styles
(a). IEEE Format:
[1] Lauretta O. Osho , Francisca Ogwueleka , Oluwafemi Osho , "Axiomatic Basis for Computer Programming," Universal Journal of Computational Mathematics(CEASE PUBLICATION), Vol. 1, No. 3, pp. 67 - 72, 2013. DOI: 10.13189/ujcmj.2013.010301.

(b). APA Format:
Lauretta O. Osho , Francisca Ogwueleka , Oluwafemi Osho (2013). Axiomatic Basis for Computer Programming. Universal Journal of Computational Mathematics(CEASE PUBLICATION), 1(3), 67 - 72. DOI: 10.13189/ujcmj.2013.010301.