Try   HackMD

(not finished … but should be readable … based on notes by Paula Severi)

Hoare logic (2018)

In Programming Languages there is an important circle of ideas including Hoare logic and Dijkstra's predicate transformer semantics, Kozen's Kleene algebra and Pratt's Dynamic logic, O'Hearn and Reynolds's Separation logic and many more methods, techniques, tools, etc.

This line of research grew out of the methodology of structured programming, which is something that every programmer learns today right from the start, but was a novel concept around 1970. I postpone a discussion of this to the conclusions.

In this lecture, we will just give some of the basic ideas and illustrate them with an important technique of proving the correctness of while programs. Therefore, an alternative title of the lecture would be

Correctness of while programs

The technique is based on a refinement of the method of invariants discussed in a previous lecture, so another possible title is

Invariants (Part 2)

These ideas have various ramifications in programming and software engineering.

  • Preconditions, Postconditions, and Invariants are useful at all levels of programming and software development: Every function, procedure, method, component, API, etc has

    • preconditions that are required from the user to guarantee correct performance
    • postconsitions that are guarantees to the user
    • invariants that are guaranteed to hold after execution if they held before execution

  • Design by contract is a software engineering method build on these ideas.

  • Check out the list of programming languages supporting these ideas.

  • Assume/guarantee or rely/guarantee is an important technique in the development of concurrent programs

I am planning to add more in the conclusions, but now let us jump into a concrete

Example

Consider the following program.

​​​​        while (x != 0 ) do z:=z+y;  x:= x-1 done

Does this program terminate?

What does the program calculate?

Does this program calculate x*y in the variable z?

It will depend on the value of x and z before executing the program.

This program will terminate and yield z = x*y at the end if x is positive and z==0 prior to it.

But how do we establish this conclusion?

And is it even correct to say that "z == x*y at the end". After all, at the end, we have x==0.

Let us think about it.

Each time the program goes through the loop x will be decremented. How often does it happen? This again depends on x.

The aim is to find a reasoning principle that frees us from tracking how often we go through a loop.

Here it is actually easy to see that we go x times through the loop (if x is not negative). But in more complicated examples there may not be a formula that allows us to caclulate the number of times we go through a loop from the available data.

(This follows from the halting problem.)

So we would like to decouple the question "how often do we go through the loop?" (termination) from the question of correctness … which is then called partial correctness, or more precisely, correctness under the assumption of termination.

Does this sound impossible?

Remember our lecture about invariants?

Can you spot an invariant? A property that remains unchanged while going throuth the loop?

Hint: Invent a notation that allows to distinguish the value of a program variable before and after the execution of some code. (There are different ways of doing this.)

Can you conclude from the invariant what the result of the computation is?

After answering the questions yourself, you can check with my solution in the footnote.[1]

Preconditions … Postconditions

As the example shows part of the difficulty lies in having a reliable notation that allows us to track change through a program and making statements (such as z == x*y ) about its properties.

The first important idea is that we want express that certain assumptions are satisfied before executing the program (preconditions) and properties that we then know after the execution of the program (postconditions)

If

S is a program ("S" as in "Sequence of Statements") then we write
{P}S{Q}

A predicate that holds before the execution of the program is called a {\em precondition} and a predicate that holds after a {\em postcondition}. If the precondition is met before execution, the program establishes the postcondition if it terminates.

For example, we can write

\colorblue{x≥0∧z=0}while (x≠0) do z:=z+y;x:=x−1 done

to express what we said above, namely that the we want to execute the program above only in case

x≥0 and
z=0.

Notation: We use mathematical notation in pre and postconditions. For example, we write "=" in

{x≥0∧z=0} to mean equality, not assignment. Program variables are typeset in typwriter font as in
x,y,z.

What should be the post condition?

Exercise: A first idea for a postcondition is

{x≥0∧z=0}while (x≠0) do z:=z+y;x:=x−1 done\colorblue{z=x∗y}.

What do you think about this? Does it look right? Consider how

x changes through the computation.

Answer.[2]

Program Variables vs Mathematical Variables

Our difficulty in finding the correct postcondition can be remedied using the following trick.

While we allow program variables to change during the execution of a program

S in
{P}S{Q}

we also allow, not in programs, but in the properties

P and
Q, mathematical variables. This is not surprising, once we had the idea, since we are already using mathematical notation such as
>,=,∧ etc. And, as in mathematics, there is no assigment-operation that would allow us to change the value of a mathematical variable. So when we write
{…n…}S{…n…}

the mathematical variable

n stands for the same value before the execution and after the execution of
S.

Exercise: What does

{y=n}S{y=n}

express about

S?

Do you think it should say that the program variable

y cannot change during the execution of the program
S? (Hint: Recall that the precondition is meant to specify a property that holds just in the moment before executing
S and that the postcondition specifies a property that holds immediately after termination of
S.)

Exercise: Do the following pre and postconditions

\colorblue{x>0 ∧ z=0 ∧ x=n}while (x≠0) do z:=z+y;x:=x−1 done\colorblue{z=n∗y}.

capture our informal discusions above?

Exercise: How do you have to change the post and precondition if you want to drop the precondition

\colorblue{z=0} and make a statement that holds for arbitrary initial values of
z?

See the footnote for a solution.[3]

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 and, therefore, the possibility of delegating such reasoning to a compiler or other verification software tools.

We will describe Hoare Logic for a minimal programming language containg only assignments, conditionals and while-loops. 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 and much more. For example, Separation logic is used by Facebook in verification tools.

While-loop

Let us go back to our leading example.

So let us try to formalise this using pre and postcondition, or, as on says, Hoare triples.

Exercise: Prove the Hoare triple

\colorblue{z=(n−x)⋅y}while (x≠0) do z:=z+y;x:=x−1 done\colorblue{z=(n−x)⋅y}.

Question: Why is

\colorblue{z=(n−x)⋅y} called a loop invariant?

Activity: Recall that the intended meaning of the while loop is to compute

z=n⋅y which we write in form of a Hoare triple as
\colorblue{z=0 ∧ x=n}while (x≠0) do z:=z+y;x:=x−1 done\colorblue{z=n⋅y}.

What reasoning steps are needed to obtain this Hoare triple from the one of the previous exercise?

To carefully explain the answer to this question takes a little effort. So let us first give a short answer:

​​​​        Show that the precondition implies the invariant and
​​​​            that the invariant implies the postcondition

First, to show that the precondition implies the invariant, is to show that

z=0 ∧ x=n ⟹ z=(n−x)⋅y

This is easy: Just replace in the conclusion

z by 0 and
x by
n and you find
0=0, which is indeed true. [4]

Second, to show that the invariant implies the postcondition, is to show that

z=(n−x)⋅y ⟹ z=n⋅y

and if you go back to the program you see that this is possible since we know that

x=0

is a postcondition that must always be true after termination of the while-loop.

Exercise: Explain why. [5]

So summarise in symbolic notation what we have done so far, we started out with a rule stating that

I is an invariant

\colorblue{I} S \colorblue{I}\colorblue{I} while B do S done\colorblue{I}

and then modified it to take into account that after termination of the loop we also know "not

B", that is,

{I} S {I}{I} while B do S done{\colorblue¬B∧I}
And then we used this rule by showing that the precondition implies
I and that
¬B∧I implies the postcondition.

This last step, which is important to bring into the picture the pre and postconditions that are actually needed for our (partial) correctness assertion, can also be formalised as a rule as follows.

\colorredP′⇒P{P} S {Q}Q⇒Q′{P′} S {Q′}
This rule is our first official rule of Hoare logic. We will see more later and they are all highlighted in red for reference.

Question: Why does this reasoning not require the precondition

\colorblue{x≥0}? For what exactly is this precondition needed?

This question has an important answer, so do look up the footnote after thinking about it yourself. [6]

Before we formulate the official rule for how to reason with a loop invariant, we need one more adjustment.

Question: Given the loop

while (x<10) do x:=x+1 done

what could we use as loop invariant?

It is easy to write down some irrelevant invariants, but which invariant would help us to prove the postcondition

\colorblue{x=10}?

A little thought shows that while an

I such that
\colorblue{I}S\colorblue{I}

is obviously an invariant for while B do S done , this is more than we need. After all, the invariant only needs to hold if we enter the loop, so it is enough for a loop invariant

I to satisfy
\colorblue{I ∧ B}S\colorblue{I}.

To illustrate this idea think about the following.

Exercise: Consider again

while (x<10) do x:=x+1 done

and find a loop invariant. Can you conclude from that invariant the postcondition

\colorblue{x=10}?

For a solution see the footnote.[7]

We are now ready to state the Hoare rule for a while loop.

The while rule is as follows.

\colorred{I∧B} S {I}{I} while B do S done{¬B∧I}

Here

I is the loop invariant.

Exercise: Use the red rules above to show

\colorblue{true} while (x<10) do x:=x+1 done\colorblue{x=10}

and

\colorblue{z=m ∧ x=n}while (x≠0) do z:=z+y;x:=x−1 done\colorblue{z=m+n⋅y}.

Making Hoare Logic Compositional

From a practical programming point of view we already learned some important lessons from studying Hoare logic.

For example, we have seen

  • how to separate termination from partial correctness and

  • how to prove partial correctness of loops using invariants.

But there is more to Hoare logic.

We have seen two examples of symbolic rules (see the red rules above) that formalise the way we reasoned about our example programs.

Two big ideas of programming languages are now the following.

  • If we can formalise enough rules needed to reason about programs, then we can build software tools that do reason for us automatically.

  • There is hope to find all rules as long as we proceed in a compositional way, that is, "by induction" on the rules that define the programming language.

In our case, we have a programming language that has assignments, sequential composition, conditionals, and while-loops.

So far we have only seen the rule for while-loops.

In what follows, we will look at rules for the other programming constructions.

Sequential Composition

The 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:
{x+1=43} y:=x+1 {y=43}
and
{y=43} z:=y {z=43}.
By putting these together, we get:
{x+1=43} y:=x+1;z:=y {z=43}
The rule for composition of programs is as follows.
\colorred{P} S {Q}{Q} T {R}{P} S;T {R}

Assignment

The assignment instruction is written as

x:=E

and it assigns the value

E to the variable
x. For example, we consider a program consisting of only one instruction
x:=y−1

which assigns

y−1 to the variable
x.

Now, suppose we know that

y has value
10 before the execution of this instruction. Then, we know that after its execution the value of
x will be
9. This is expressed in Hoare Logic as follows.
\colorblue{y=10}   x:=y−1   \colorblue{x=9}

The predicate

y=10 is the precondition and the predicate
x=9 is the postcondition.

Our predicates could involve more variables. For instance,

\colorblue{x>0∧x≤3∧y=10}   x:=y−1  \colorblue{x=9∧y=10}

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

\colorred{P[E/x]}   x:=E   {P}

In other words, the post-condition

P holds after the execution of the assignment
x:=E provided that
P[E/x] holds prior to it.

Suppose now that the program is the statement

y:=x+1

and we want that

y=43 after its execution. What are the possible values for
x at the beginning of the execution of our program?

Using the assignment axiom we get that

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

The precondition

x+1=43 can be simplified to
x=42. Hence,
\colorblue{x=42}   y:=x+1   \colorblue{y=43}

Suppose now that our program is the statement

x:=x+1

and we want that

x≤N after its execution. Using the assignment axiom we get
\colorblue{x+1≤N}   x:=x+1   \colorblue{x≤N}

Hence,

\colorblue{x<N}   x:=x+1   \colorblue{x≤N}

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

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

The above statement is not true if

x and
y refer to the same variable, because no precondition can cause y to be 3 after x is set to 2.

If-then-else

Consider the following program.

if (y>0) then x:=y else x:=−y endif

We want to show that the above program calculates the absolute value of

y,
denoted by
|y|, i.e.
{true}if (y>0) then x:=y else x:=−y endif{x=|y|}

If

y>0 then it is clear that
x=y. If not, then
y≤0
and then
x=−y=|y|.

Consider the following program.

if (x≥y) then z:=x else z:=y endif
We want to show that the above program calculates the maximum of the
two values
x and
y, i.e.
{true}if (x≥y) then z:=x else z:=y endif{z=max(x,y)}
If
x≥y then
x is the maximum and then
z=x=max(x,y). If not, then
x<y and
z=y=max(x,y).

The conditional rule is as follows.

\colorred{B∧P} S {Q}{¬B∧P} T {Q}{P} if B then S else T endif {Q}

Summary and Outlook

I will first summarise some of the lessons that we learned from studying Hoare logic, lessons that are relevant to programmers and software engineers far beyond the particularities of this specific approach to program correctness.

Then I will briefely look at the history of ideas around "structured programming" which gave rise to Hoare logic and other approaches to program verification.

Hoare Logic

… the following summary is currently just a collection of random notes …

  • The following habits can improve the practice of programming

    • What are the pre and postconditions of the code I write?
    • Should I test them explicitely? Raise an exception if they are violated? Describe them explicitely in comments? Make users of my code aware of them?
    • Using software tools that support pre and postcondition in my code.
    • Thinking of loop-invariants before implementing my loops.
    • Working backwards from postconditions to preconditions: Given that I want to guarantee a postcondition, what are the preconditions and what is the code needed for this? [8]

  • These programming techniques have formal counterparts, some of which are

    • Hoare triples
    • loop invariants
    • rules of Hoare logic

  • Hoare logic is compositional
    We have seen that each programming construct corresponds to a rule in Hoare logic for a simple programming language consisting only of assignments, conditionals, sequential composition and while-loops. In principle there is no reason why this approach could not be extended to cover any construct available in any programming language. Not surprisingly, the literature on this topic is vast. For us here, the upshot is that the rules of Hoare logic are compositional in the definition of the syntax of the language.

  • Hoare logic is a formal system
    While this lecture emphasised how to use invariants to reason about the correctness of while loops, we also hinted at how this reasoning can be formalised.

  • Hoare logic can be implemented by software tools that support program design and development
    This is a consequence of the previous item. Formal systems can be implemented and then turned into tools.

  • Hoare logic as many ramifications for various special purpose situations such as concurrency, memory management, etc

Structured Programming

(this section is being written as an after-thought and was not part of the semester)

Early programming close to the machine relies on jumps as a basic mechanism to control flow. Accordingly, early higher level languages such as Fortran had a corresponding

goto statement. Goto's lend themselves to the writing of "unstructured" code that is difficult to read and debug, but was considered a necessary ingredient.

In 1966, an article by Bohm and … showed that jumps are not needed when … tbc …

Further Reading

Formal Verification

We have seen that the rules of Hoare logic can be formalised in symbolic notation. It should therefore should be possible to implement software engineering tools that automate reasoning about programs.

To get a taste of how verification is done in real world programming applications, have a look at the blogs by David Crocker about Verifying loops in C and C++, part 1 and part 2 and part 3. There is also a very short introduction to software verification.

  1. What about

    z=(n−x)⋅y where
    n     is the value of
    x     before entering the loop?
    The first trick here is to use two different variables: program variables
    x,y,z     that can change during program execution and mathematical variables
    n     that cannot.
    The second trick is that we can conclude the value of
    z     after the loop finishes by taking the conjunction of the loop-invariant
    z=(n−x)∗y     with the negation
    x=0     of the condition (x != 0) that allows the entry into the loop. After all, we can only finish the loop if we are not allowed entry. But now see what happens. This conjunction implies
    z=n⋅y    , which is what we wanted (remember that
    n     is the value of
    x     before the loop was entered). ↩︎

  2. The problem with

    \colorblue{z=x∗y} is that it only gives what we want if take for
    x     the value of
    x     before the computation and for
    z     the value of
    z     after the computation. On the other hand, if we take for both variables their values after the computation, as we should, the condition
    \colorblue{z=x∗y}     is false (for almost all initial values of the variables). ↩︎

  3. \colorblue{x>0 ∧ z=m ∧ y=n}while (x≠0) do z:=z+y;x:=x−1 done\colorblue{z=m+n∗y}. ↩︎

  4. The rule of logic that allows to replace equals by equals is one of the most basic rules that we typically use without feeling the need to formulate it explicitely, as we did in the example of equational reasoning under the name of "congruence rule". ↩︎

  5. The condition

    B that forces to execute the loop is in our example x!=0, that is,
    ¬(x=0)    . Therefore
    ¬B     is
    ¬¬(x=0)    , which is
    x=0    . ↩︎

  6. Our first observation was that the precondition

    {x≥0} is needed for correctness. Why is it not needed in the proof of the Hoare triple? The reason is that Hoare triples only concern what is called partial correctness, that is, correctness under the assumption of termination. Indeed,
    {x≥0}     is only needed in our example to argue for termination. ↩︎

  7. \colorbluex≤10 is a loop invariant ↩︎

  8. Note that this goes in the opposite direction of our usual thinking about code, which is operational and proceeds from an initial state and works forward from there. ↩︎

Last changed by 
 
Alexander Kurz
0
444
Published on HackMD