霍尔逻辑是一套由英国计算机科学家霍尔（ C. A. R. Hoare）开发的形式系统，后来又通过他与其它研究者做了进一步的精细化处理，这个系统的构建目的是用来推理验证程序的正确性，用数学的严格性做保证。
            It was published in Hoare's 1969 paper,^[1] where Hoare acknowledges earlier contributions from Robert Floyd, who had published a similar system^[2] 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 P and Q are assertions and C is a command. P is called the precondition and Q the postcondition: if the precondition is met, the command establishes 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.

           

Rules

Empty statement axiom schema

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:

Here P[E / x] 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[E / x]} is equivalent to the after-assignment truth of {P}. Thus if {P[E / x]} were true prior to the assignment, by the assignment axiom then {P} will be true subsequent to that assignment. Conversely, if {P[E / x]} were false prior to the assignment statement, {P} must then be false following the assignment.

Examples of valid triples include:

• 
• 

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

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.

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

and

By the sequencing rule, one concludes:

Conditional rule

Consequence rule

While rule

Here P is the loop invariant.

While rule for total correctness

In this rule, in addition to maintaining the loop invariant, one also proves termination by way of a term, called the loop variant, here t, whose value strictly decreases with respect to a well-founded relation during each iteration. Note that, given the invariant P, the condition B must imply that t is not a minimal element of its range, for otherwise the premise of this rule would be false. Because the relation "<" is well-founded, each step of the loop is counted by decreasing members of a finite chain. Also note that square brackets are used here instead of curly braces to denote total correctness, i.e. termination as well as partial correctness. (This is one of various notations for total correctness.)

Examples

Example 1
			(Assignment Axiom)
			(Consequence Rule)
Example 2
			(Assignment Axiom)
			( for x, N with integer types.)
			(Consequence Rule)

信息来源:   http://en.wikipedia.org/wiki/Hoare_logic

转载本文请联系原作者获取授权，同时请注明本文来自黄富强科学网博客。
链接地址：https://blog.sciencenet.cn/blog-89075-231985.html

上一篇：Digital native
下一篇：Oracle's Support for Open Source and Open Standards