Hoare logic (also known as Floyd–Hoare logic or Hoare rules) is a
formal system
A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system.
A fo ...
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
Robert W Floyd (June 8, 1936 – September 25, 2001) was a computer scientist. His contributions include the design of the Floyd–Warshall algorithm (independently of Stephen Warshall), which efficiently finds all shortest paths in a graph and ...
, who had published a similar system for
flowchart
A flowchart is a type of diagram that represents a workflow or process. A flowchart can also be defined as a diagrammatic representation of an algorithm, a step-by-step approach to solving a task.
The flowchart shows the steps as boxes of ...
s.
Hoare triple
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''.
[Hoare originally wrote "" rather than "".] 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,
jump
Jumping is a form of locomotion or movement in which an organism or non-living (e.g., robotic) mechanical system propels itself through the air along a ballistic trajectory.
Jump or Jumping also may refer to:
Places
* Jump, Kentucky or Jump S ...
s, and
pointers.
Partial and total correctness
Using standard Hoare logic, only
partial correctness can be proven.
Total correctness additionally requires
termination
Termination may refer to:
Science
*Termination (geomorphology), the period of time of relatively rapid change from cold, glacial conditions to warm interglacial condition
*Termination factor, in genetics, part of the process of transcribing RNA ...
, which can be proven separately or with an extended version of the While rule.
[) Here: Sect. 3.4, p. 64.] 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. In his 1969 paper, Hoare used a narrower notion of termination which also entailed the absence of implementation limit violations, and expressed his preference for the broader notion of termination as it keeps assertions implementation-independent:
Rules
Empty statement axiom schema
The
empty statement rule asserts that the statement does not change the state of the program, thus whatever holds true before also holds true afterwards.
[This article uses a natural deduction style notation for rules. For example, informally means "If both and hold, then also holds"; and are called antecedents of the rule, is called its succedent. A rule without antecedents is called an axiom, and written as .]
:
Assignment axiom schema
The assignment axiom states that, after the assignment, any predicate that was previously true for the right-hand side of the assignment now holds for the variable. Formally, let be an assertion in which the variable is
free. Then:
:
where