Hoare logic

Hoare logic

Hoare logic (also known as Floyd–Hoare logic) is a formal system developed by the British computer scientist C. A. R. Hoare, and subsequently refined by Hoare and other researchers. The purpose of the system is to provide a set of logical rules in order to reason about the correctness of computer programs with the rigour of mathematical logic.

It was published in Hoare's 1969 paper, [C. A. R. Hoare. " [http://sunnyday.mit.edu/16.355/Hoare-CACM-69.pdf An axiomatic basis for computer programming] ". "Communications of the ACM", 12(10):576–585, October 1969. doi|10.1145/363235.363259] where Hoare acknowledges earlier contributions from Robert Floyd, who had published a similar system [R. W. Floyd. " [http://laser.cs.umass.edu/courses/cs521-621.Spr06/readlings/Floyd.pdf Assigning meanings to programs.] " Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Vol. 19, pp. 19–31. 1967.] 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

:{P};C;{Q}

where "P" and "Q" are "assertions" and "C" is a "command". "P" is called the "precondition" and "Q" the "postcondition". Assertions are formulas in predicate logic.

Hoare logic has 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.

Partial and total correctness

Standard Hoare logic proves only partial correctness, while termination would have to be proved separately. Thus the intuitive reading of a Hoare triple is: Whenever "P" holds of the state before the execution of "C", then "Q" will hold afterwards, or "C" does not terminate. Note that if "C" does not terminate, then there is no "after", so "Q" can be any statement at all. Indeed, one can choose "Q" to be false to express that "C" does not terminate.

Total correctness can also be proven with an extended version of the While rule.

Rules

Empty statement axiom schema

: frac{}{{P} extbf{skip} {P !

Assignment axiom schema

The assignment axiom states that after the assignment any predicate holds for the variable that was previously true for the right-hand side of the assignment:

: frac{}{{P [x/E] } x:=E {P} } !

Here P [x/E] denotes the expression "P" in which all free occurrences of the variable "x" have been replaced with the expression "E".

The meaning of the assignment axiom is that the truth of {P [x/E] } is equivalent to the after-assignment truth of {P}. Thus if {P [x/E] } were "true" prior to the assignment, by the assignment axiom then {P} will be "true" subsequent to that assignment. Conversely, if {P [x/E] } were "false" prior to the assignment statement, {P} must then be "false" following the assignment.

Examples of valid triples include:

:*{x+1 = 43} y:=x + 1 { y = 43 }!:*{x + 1 leq N } x := x + 1 {x leq N} !

The assignment axiom proposed by Hoare "does not apply" when more than one name can refer to the same stored value. For example,

:{ y = 3} x := 2 {y = 3 }

is not a true statement if "x" and "y" refer to the same variable, because no precondition can cause "y" to be 3 after "x" is set to 2.

Rule of composition

Hoare's rule of composition applies to sequentially-executed programs "S" and "T", where "S" executes prior to "T" and is written "S;T".

: frac {{P} S {Q} , {Q} T {R} } {{P} S;T {R !

For example, consider the following two instances of the assignment axiom:

:{ x + 1 = 43} y:=x + 1 {y =43 }

and

:{ y = 43} z:=y {z =43 }

By the sequencing rule, one concludes:

:{ x + 1 = 43} y:=x + 1; z:= y {z =43 }

Conditional rule

:frac { {B wedge P} S {Q} , { eg B wedge P } T {Q} } { {P} extbf{if} B extbf{then} S extbf{else} T extbf{endif} {Q} } !

While rule

:frac { {P wedge B } S {P} } { {P } extbf{while} B extbf{do} S extbf{done} { eg B wedge P} }!

Here "P" is the loop invariant.

Consequence rule

:frac { P^prime ightarrow P , lbrace P brace S lbrace Q brace , Q ightarrow Q^prime } { lbrace P^prime brace S lbrace Q^prime brace }!

While rule for total correctness

::frac { {P wedge B wedge t = z } S {P wedge t < z } , P ightarrow t geq 0} { {P } extbf{while} B extbf{do} S extbf{done} { eg B wedge P} }! Fact|date=August 2008

In this rule, in addition to maintaining the loop invariant, one also proves termination by way of a term, called the loop variant, whose value decreases during each iteration, here "t". Note that "t" must take values from a well-founded set, so that each step of the loop is counted by decreasing members of a finite chain.

Examples

:

See also

* Design by contract
* Dynamic logic
* Edsger W. Dijkstra
* Predicate transformer semantics
* Program verification
* Static code analysis
* Loop invariant

References

Further reading

* Robert D. Tennent. " [http://www.cs.queensu.ca/home/specsoft/ Specifying Software] " (a recent textbook that includes an introduction to Hoare logic) ISBN 0-521-00401-2

External links

* [http://isabelle.in.tum.de/Bali/ Project Bali] has defined Hoare logic-style rules for a subset of the Java programming language, for use with the Isabelle theorem prover
* [http://www.key-project.org/download/hoare/ KeY-Hoare] is a semi-automatic verification system built on top of the KeY theorem prover. It features a Hoare calculus for a simple while language.
* [http://j-algo.binaervarianz.de/index.php?language=en j-Algo-modul Hoare calculus] &mdash; A visualisation of the Hoare calculus in the in the algorithm visualisation program j-Algo


Wikimedia Foundation. 2010.

Поможем сделать НИР

Look at other dictionaries:

  • Hoare — is the name of: * C. A. R. Hoare (b. 1934), British computer scientist, creator of Hoare logic and the Quicksort sorting algorithm * Kelly Hoare (b. 1963), Australian politician * Mike Hoare (b. 1920), Irish mercenary leader * Prince Hoare… …   Wikipedia

  • Logic in computer science — describes topics where logic is applied to computer science and artificial intelligence. These include:*Investigations into logic that are guided by applications in computer science. For example: Combinatory logic and Abstract interpretation;… …   Wikipedia

  • Hoare-Logik — Der Hoare Kalkül (auch Hoare Logik) ist ein Formales System, entwickelt von dem britischen Informatiker C. A. R. Hoare und später verfeinert von Hoare und anderen Wissenschaftlern. Er wurde 1969 in einem Artikel mit dem Titel An axiomatic basis… …   Deutsch Wikipedia

  • Hoare-Tripel — Der Hoare Kalkül (auch Hoare Logik) ist ein Formales System, entwickelt von dem britischen Informatiker C. A. R. Hoare und später verfeinert von Hoare und anderen Wissenschaftlern. Er wurde 1969 in einem Artikel mit dem Titel An axiomatic basis… …   Deutsch Wikipedia

  • Logic — For other uses, see Logic (disambiguation). Philosophy …   Wikipedia

  • Category:Logic in computer science — Logic in computer science is that branch of mathematical logic which is approximately the intersection between mathematical logic and computer science. It contains: Those investigations into logic that are guided by applications in computer… …   Wikipedia

  • Dynamic logic (modal logic) — For the subject in digital electronics also known as clocked logic, see dynamic logic (digital electronics). Dynamic logic is an extension of modal logic originally intended for reasoning about computer programs and later applied to more general… …   Wikipedia

  • Tony Hoare — Sir Charles Antony Richard Hoare Sir Charles Antony Richard Hoare giving a conference at the EPFL on 20 June 2011 Born …   Wikipedia

  • C. A. R. Hoare — Infobox Scientist name = Charles Antony Richard Hoare image width = 150px birth date = birth date and age|1934|1|11 birth place = Colombo, Sri Lanka field = Computer Scientist work institution = Elliott Brothers Queen s University of Belfast… …   Wikipedia

  • Separation logic — Separation Logic, a term attributed to John C. Reynolds, is an extension of Hoare logic that describes variations on program logic in computer science.In particular, separation logic facilitates reasoning about:* programs that manipulate pointer… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”