This paper presents an axiomatic basis for computer programming, focusing on proving the correctness of programs using formal methods. It discusses the use of axiomatic semantics to derive mathematical verification conditions from computer programs. The paper presents axioms for sequential flow, iteration (while...do and do...while), and alternation (if...else) flows. 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 also discusses the limitations of traditional testing methods, which often fail to detect all errors in complex programs. It emphasizes the need for complementary methods, such as formal methods, to ensure program correctness. The axiomatic method is highlighted as a formal approach that provides a basis for measuring the quality of programming languages and supports the intuitive judgment of programmers. The paper reviews related works, including methods like Floyd's method, Hoare logic, and structural induction, which are used for proving program correctness. It also discusses the difference between partial and total correctness, with total correctness including loop termination. The mathematical foundations of the axiomatic method are outlined, including the axioms for integers and the definitions of notations used in axiomatic proofs. The paper provides axioms for assignment, iteration (while...do and do...while), and alternation (if...else), and demonstrates their application in proving the correctness of integer multiplication programs. Two programs for integer multiplication are presented: one using repeated addition and another using a more efficient method based on binary decomposition. Both programs are proven correct using axiomatic methods. The paper concludes that axiomatic methods complement the intuitive judgment of programmers and are essential for ensuring program correctness. It also notes that other methods, such as fixpoint induction, coinduction, and computer tools like ESC/Java, SPARK, and Dafny, are being used to prove program correctness.This paper presents an axiomatic basis for computer programming, focusing on proving the correctness of programs using formal methods. It discusses the use of axiomatic semantics to derive mathematical verification conditions from computer programs. The paper presents axioms for sequential flow, iteration (while...do and do...while), and alternation (if...else) flows. 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 also discusses the limitations of traditional testing methods, which often fail to detect all errors in complex programs. It emphasizes the need for complementary methods, such as formal methods, to ensure program correctness. The axiomatic method is highlighted as a formal approach that provides a basis for measuring the quality of programming languages and supports the intuitive judgment of programmers. The paper reviews related works, including methods like Floyd's method, Hoare logic, and structural induction, which are used for proving program correctness. It also discusses the difference between partial and total correctness, with total correctness including loop termination. The mathematical foundations of the axiomatic method are outlined, including the axioms for integers and the definitions of notations used in axiomatic proofs. The paper provides axioms for assignment, iteration (while...do and do...while), and alternation (if...else), and demonstrates their application in proving the correctness of integer multiplication programs. Two programs for integer multiplication are presented: one using repeated addition and another using a more efficient method based on binary decomposition. Both programs are proven correct using axiomatic methods. The paper concludes that axiomatic methods complement the intuitive judgment of programmers and are essential for ensuring program correctness. It also notes that other methods, such as fixpoint induction, coinduction, and computer tools like ESC/Java, SPARK, and Dafny, are being used to prove program correctness.