Hoare logic and its role in computer programs

Document Type : Academic research papers

Authors

1 Faculty of women Ain shams university

2 Professor of Logic and Philosophy of Science Girls College For Arts, Science & Education Ain Shams University

3 Assistant Professor of Logic, Women's College For Arts, Science & Education Ain Shams University

Abstract

Designing and developing high-quality systems that meet their requirements is extremely important. Especially with the ever-increasing complexity of computer systems, failure of the system in its mission or safety can cause many problems such as: cost overruns, loss of life or severe economic losses; Therefore, many scientists have directed their attention to detecting errors in these programs and treating them, based on sound logical foundations. Hoare’s logic is considered the first logic that presented a formal format for application in the field of formal verification of the verification of the program. Therefore, this research aims to clarify and explain the role of Hoare’s logic in verifying the program. By identifying the reasons for its appearance, the stages of its development, its concept, presenting and analyzing the components of its formal format, and explaining how to apply it in verifying the validity of the program. The researcher followed the historical approach and the comparative critical analytical approach. It becomes clear to us that logic is not separated from reality, but rather keeps pace with it considering scientific and technological progress. In addition, computer science students cannot do without studying logic; It provides them with the basis for understanding how computers work, and how to deal with them. If the programmer wants to avoid errors in the code and verify the validity of his program, he must apply the foundations and rules of Hoare's logic.

Keywords

Main Subjects

Buhūth
Volume 4, Issue 5
issue 5 Social Sciences and Humanities and languages 2024
May 2024
Pages 164-197

Files

Share

How to cite

Statistics