Hoare Logic

History

In October 1969, Hoare published, in the "Communications of the ACM" a paper entitled "An Axiomatic Basis for Computer Programming." He stated that "in this paper an attempt is made to explore the logical foundations of computer programming by use of techniques which were first applied in the study of geometry and have later been extended to other branches of mathematics." The purpose of the paper was to provide a set of logical rules to reason about the correctness of computer programs.

In 1967, Robert Floyd had published his paper, entitled 'Assigning Meaning to Programs' in 'Proceedings of the American Mathematical Society Symposia on Applied Mathematics.' In this paper, he attempted to provide formalized definitions of programs 'in such a way that a rigorous standard is established for proofs about computer programs, including proofs of correctness, equivalence, and termination.'

Yet the fundamental difference between Floyd's work and the work of Hoare is the notation – whereas Hoare uses logical formulae in axiomatic semantics, Floyd used flow charts as illustrated. Floyd's formalization was greatly more time consuming, and had to be done by hand.

Verification & Correctness

"And the final question is 'How do we know that the program is in fact correct?' The theory of programming tells us that this final assurance can in principle be given by mathematical reasoning and proof, guaranteeing that the specifications are a logical consequence of the text of the program. This theory has already been put into practice. Since the earliest times, proofs for small and critical programs have been constructed manually, and checked by human eye. In some cases, the proofs have been constructed as part of the development process for the software. More recently, the reliability and effectiveness of the verification has been increased by automation of the construction or the checking of the proofs. In analogy with other branches of science, consider the text of the program as the experimental data; consider the specifications of the external and internal interfaces of the program as a theory of how and why the program works. Now an automatic tool for program verification is one that checks the consistency of the theory with the actual text of the program, just like the analysis tools of other branches of science and engineering. Its application greatly increased confidence that the verified program when executed will conform to specification. That is the dream that has for over thirty years driven research in basic Computing Science."
Tony Hoare - 'The Ideal of Program Correctness' (May 06)

Formal verification is the proving or disproving the correctness of algorithms with respect to a certain formal specification. Correctness of programs is asserted when programs are correct with respect to a specification. We specify mathematically precisely what the program is intended to do, for all possible inputs (this is the "specification"). Since Hoare's work, this has been based on axiomatic semantics. Correctness can be asserted when programs fulfill the specification. We can verify this by building on algorithms using rules of inference until they match or do not match the required specification.

We need to make a distinction between total correctness, which requires that the program terminates, and partial correctness, which simply requires that if an answer is returned (i.e. the program terminates) it will be correct. Given the existence of the halting problem (no program can be written which can determine whether any other arbitrary program halts for all possible inputs), total correctness is more of a problem (we can actually use the While Rule for some programs to satisfy total correctness). From this point onwards, we will deal only with partial correctness.

Why 3+2 can equal 1
When we formalize axioms and inferences that we need in order to prove program correctness, care must be taken to choose the correct axioms. One particular case is with regard to arithmetic. Mathematical and computational arithmetic may differ - whereas mathematical arithmetic deals with an infinite set of integers, computational arithmetic deals with a finite set. Thus we must choose an axiom to deal with overflow.

We can use a simple example to illustrate this fact. If our set of integers is 0, 1, 2, 3, then when a result is a number greater than 3 (or less than 0), the choice of axiom will determine the value. It is important this corresponds to the behaviour of the program. There are 3 choices:

  1. Strict interpretation: max + 1 = * (if out of bounds does not exist)
  2. Firm boundary: max + 1 = max (if go over max, value = max)
  3. Modulo Arithmetic: max + 1 = 0 (restart at max + 1 =0, so max + 2 = 1 etc.)
So, if we were trying to calculate, with the only defined numbers as 0, 1, 2, 3,
3 + 2 =
  • Strict interpretation 3+2 = *
  • Firm bond 3+2 = 3
  • Modulo Arithmetic 3+2 = 1
It is therefore important the correct axioms are used.

How It Works

We take a program, and formalize it using Hoare triples:

P { C } Q

P: Precondition (an assertion in Predicate Logic)
C: Command - the program
Q: Postcondition (an assertion in Predicate Logic)

What does this say?
Whenever 'P' holds for a state before the execution of the command, C, then
a) Q will hold afterwards, or,
b) C does not terminate (in this case, there would be no postcondition at all, so to make the expression true, Q could be anything. In fact to show that C does not terminate, if we know the triple is correct, we can just show that Q is false)

A simple example:
P: x + 12 = 652
C: y = x + 12
Q: y = 652

x + 12 = 652 {y = x + 12} y = 652
This utilizes a common rule we all recognize - that of assignment i.e. where we see a y in the postcondition, we assign the value given in the command (x + 12) to find the precondition.

To prove more complex programs, we need to use more axioms and inferences.

A Sample of Rules

We can now have a look at some of the rules that Hoare introduces which we can use to work with programs.

  1. Assignment
    What is it? The setting or resetting of a value stored in a storage location denoted by a variable name.
    x: an identifier for a simple variable
    f: a side-effect-free expression of a programming language, possibly containing x

    Expressed formally: |- P[x/f] {x:=f} P
    The above axiom describes an infinite set; it shows a common pattern.

    Logic to English translations: P[x/f] is found by substituting 'f' for all occurrences of 'x' in P.
    |- is a syntactic turnstile. This reads 'there is no situation in which the statement before the turnstile can be true and the statements after the turnstile false simultaneously.' If there is nothing before the turnstile, this is a syntactic theorem - there is no situation in which the statement after the turnstile can be false.

    e.g. x + 3 = 21 { y := x + 3 } y = 21
    In this example, every instance of ‘x+3’ in the precondition has been replaced by 'y' to form the postcondition.
  2. Consequence
    We need rule of inference to prove new things. The rule of consequence allows us to extend inferences.

    Expressed formally: [P {Q} R] & [R -> S] |- P {Q} S

    More translations:
    R -> S is a material implication. The important property here is that in the case in which R is true, S will always also be true.

    We can extend this:
    [P' -> P] & [R -> S] & [S-> S'] & [P{Q}R] |- P'{Q}S'
    The precondition that is least restrictive on variables is the weakest precondition and can enable simplification of the proof.

  3. The rule of composition allows us to 'merge' two programs into one, when the postcondition of the first is the same as a precondition of the second.

    Expressed formally: [P {S} Q] & [Q {T} R] |- P {S, T} R

    If the proven postcondition (result) of the first program (in this case Q) is identical to the precondition of the 2nd program (Q) under which the 2nd program produces its intended result (R), then the whole will produce the intended result (R), provided the precondition of the first part (P) is satisfied.
  4. Other rules
    Hoare also detailed other useful inferences, and more have been developed since the original work was published in 1969. We will one such encounter one such rule - the conditional rule - below.

    A Complex Example

    We shall try to prove that a piece of programming language is correct. The program we shall look at intends to produce the maximum value from two variables e.g. if the variables were '12' and '65' the program would output '65.' This requires multiple application of a number of different rules of inference.

    We can represent this "max" function using C++ Lite programming language:
    int Max (int a, int b) {
    int m;
    if (a >=b)
    m = a;
    else
    m = b;
    return m;
    }

    We can also describe the "max" function declaratively as follows: Q ? [m = max (a,b)]

    Note however, the predicate here describes only what the result should be, rather than how the result should be computed. We need to prove that the postcondition, Q, actually occurs in reality.

    To prove that the program works, we have two choices:
    1. Trial and error. We could use a variety of input variables, and test to see whether the program works. However, this only ever provides evidence for correctness, not proof for correctness. "Testing can show the presence of errors, but not their absence" (E.W. Dijkstra). It is also deeply time consuming - like squashing insects one-by-one. 2. Axiomatic semantic analysis - Hoare's concept. We use Hoare triples, as explained above. Each triple consists of three parts - a precondition, command and postcondition.

    In this case, we have a postcondition, Q, which we are trying to prove is correct [m = max (a,b)].We also have a precondition, P. With this function, any set of input values is possible - no restrictions are necessary - thus we can call the precondition 'true.'

    We shall use simple rules to derive the solution. Our specification (i.e. the precise mathematical explanation of the intended function the program should compute) is:
    true {if (a >= b) m = a; else m=b;} m = max (a,b)

  1. Assignment
    The assignment rule tells us that the following triple is valid:
    a = max (a,b) {m = a} m = max (a,b)
    Why? We can work backwards from our postcondition, already established (m = max (a,b)) using a command of 'm = a'
  2. Consequence
    {a>b} => {a = max (a,b)}
    We can therefore strengthen the precondition, ensuring this triple is valid:
    a>b {m = a} m = max (a,b)
  3. Assignment and Consequence again - on the 'if' part of the statement
    We can perform the same processes using an initial command of m = b rather than m = a.
    This gives us the result:
    aFurther use of consequence
    We now have two separate triples:
    a>b {m = a} m = max (a,b) &
    a
    We can state that a > b & true => a > b
    And also that b < a => b < a & true

    Thus we can utilize the rule of consequence again to produce:
    a > b & true {m = a} m = max (a,b) &
    a < b & true {m = b} m = max (a,b)
  4. Merge together the two - use rule of conditionality
    Conditional rule:
    [B & P {S} Q] &
    [~B & P {T} Q]
    |- [P {if B then S; else T} Q]

    a>b & true {m = a} m = max (a,b) &
    a
    B: a>b
    P: true
    S: m=a
    Q: m = max (a,b)
    T: m=b

    true {if )a>=b) m = a; else m=b;} m = max (a,b)

    Goal is:
    true {if (a >= b) m = a; else m=b;} m = max (a,b)

    Success!