Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of GraphSearch.
Concept
Hoare logic
Summary
Hoare logic (also known as Floyd–Hoare logic or Hoare rules) is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and logician Tony Hoare, and subsequently refined by Hoare and other researchers. The original ideas were seeded by the work of Robert W. Floyd, who had published a similar system for flowcharts.
The central feature of Hoare logic is the Hoare triple. A triple describes how the execution of a piece of code changes the state of the computation. A Hoare triple is of the form
where and are assertions and is a command. is named the precondition and the postcondition: when the precondition is met, executing the command establishes the postcondition. Assertions are formulae in predicate logic.
Hoare logic provides axioms and inference rules for all the constructs of a simple imperative programming language. In addition to the rules for the simple language in Hoare's original paper, rules for other language constructs have been developed since then by Hoare and many other researchers. There are rules for concurrency, procedures, jumps, and pointers.
Using standard Hoare logic, only partial correctness can be proven. Total correctness additionally requires termination, which can be proven separately or with an extended version of the While rule. Thus the intuitive reading of a Hoare triple is: Whenever holds of the state before the execution of , then will hold afterwards, or does not terminate. In the latter case, there is no "after", so can be any statement at all. Indeed, one can choose to be false to express that does not terminate.
"Termination" here and in the rest of this article is meant in the broader sense that computation will eventually be finished, that is it implies the absence of infinite loops; it does not imply the absence of implementation limit violations (e.g. division by zero) stopping the program prematurely.
Official source
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.