This paper presents an axiomatic basis for computer programming, focusing on proving the correctness of programs using formal methods. The paper discusses axiomatic semantics, a formal method that uses proof rules to extract mathematical verification conditions from a program. The axioms of program flow, including sequential flow, iteration, and alternation flows, are presented. Using these axioms, the completeness of two variants of integer multiplication programs is proved. The results show that computer programs can be verified for correctness without necessarily testing them, complementing testing in practice. The paper begins by discussing the importance of program correctness, which is closely tied to the correctness of algorithms and the absence of errors in program code. It emphasizes the need for complementary methods to achieve program correctness, as testing alone is insufficient for large and complex programs. The axiomatic method is introduced as a formal approach to proving program correctness, with self-evidence and obviousness as key characteristics. The paper then reviews related works, highlighting various methods used to prove program correctness, including recursion induction, structural induction, and Floyd-Hoare logic. It discusses the distinction between partial and total correctness, with total correctness requiring both partial correctness and loop termination. The mathematical foundations of the axiomatic method are outlined, including the axioms for integers and the definitions of notations used in the axiomatic approach. The paper presents axioms for assignment, iteration (while...do and do...while), and alternation (if...else) statements. These axioms are used to prove the correctness of the two integer multiplication programs. The first program uses repeated addition to multiply two integers, and the second program uses a more efficient method based on binary decomposition. Both programs are proven correct using the axiomatic method, demonstrating the effectiveness of formal methods in verifying program correctness. The paper concludes that axiomatic methods complement the intuitive judgment of programmers, and that further research can explore the application of these methods to more complex programs.This paper presents an axiomatic basis for computer programming, focusing on proving the correctness of programs using formal methods. The paper discusses axiomatic semantics, a formal method that uses proof rules to extract mathematical verification conditions from a program. The axioms of program flow, including sequential flow, iteration, and alternation flows, are presented. Using these axioms, the completeness of two variants of integer multiplication programs is proved. The results show that computer programs can be verified for correctness without necessarily testing them, complementing testing in practice. The paper begins by discussing the importance of program correctness, which is closely tied to the correctness of algorithms and the absence of errors in program code. It emphasizes the need for complementary methods to achieve program correctness, as testing alone is insufficient for large and complex programs. The axiomatic method is introduced as a formal approach to proving program correctness, with self-evidence and obviousness as key characteristics. The paper then reviews related works, highlighting various methods used to prove program correctness, including recursion induction, structural induction, and Floyd-Hoare logic. It discusses the distinction between partial and total correctness, with total correctness requiring both partial correctness and loop termination. The mathematical foundations of the axiomatic method are outlined, including the axioms for integers and the definitions of notations used in the axiomatic approach. The paper presents axioms for assignment, iteration (while...do and do...while), and alternation (if...else) statements. These axioms are used to prove the correctness of the two integer multiplication programs. The first program uses repeated addition to multiply two integers, and the second program uses a more efficient method based on binary decomposition. Both programs are proven correct using the axiomatic method, demonstrating the effectiveness of formal methods in verifying program correctness. The paper concludes that axiomatic methods complement the intuitive judgment of programmers, and that further research can explore the application of these methods to more complex programs.