Exercise 13: Hoare Logic

These exercises build on the material you developed for the previous exercise set. Load this first before extending it in these exercises.

Hoare Triples

Hoare logic is a simple logic for proving properties of programs. It was developed by C. A. R. Hoare in the late 1960s. The classic introduction to Hoare logic is Hoare's original paper (note the standard notation has changed a little since then):

C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576-585, October 1969.

Hoare's original approach was to describe a set of logical rules that should hold true of a programming language, this implies a meaning for programs in the language. This technique for assigning meaning to programming languages is known as an axiomatic semantics. Axiomatic semantics have fallen out of favour because the indirectness of the technique makes it all too easy to get wrong. However, the rules of Hoare logic are a natural way to reason about programs. A more modern approach is to first describe a more direct semantics for the programming language, as we did in the last set of exercises, and then prove that programs in the language support the Hoare logic rules. This is the subject of this exercise set.

An expression in Hoare logic, also known as a Hoare triple, looks like this:

{P} C {Q}

In this notation P and Q are a predicates (or functions from the state space to boolean) and C is a command (or program). The meaning of this expression is that if the command C is run in a state in which the predicate P holds, then Q will hold in any state C terminates in. This gets a little bit simpler for the programming language you defined in the last set of exercises because it is deterministic and does not allow loops. This means that for any initial state a program must terminate, and there is only one final state it can terminate in.

You cannot define mix-fix notation, like Hoare triples, in HOL, so we will have to come up with a different notation. While we are about it we'll make another improvement. It is clear that if we are going to be using Hoare logic then we are going to need to write lots of state predicates (functions from states to booleans), as in P and Q above. We could do this using lambda-expressions, but this would be a pain, especially when we have already defined a syntax for boolean expressions and a meaning function, Mb, that interprets them as state predicates. Define a HOL function HOARE to capture the meaning of a Hoare triple. Your function should take a boolean expression representing a predicate on the initial state, a command, and a boolean expression representing a command on the final state. That is, HOARE P C Q should hold if for any initial state satisfying the meaning of P, the meaning of Q is satisfied in the final state reached under the meaning of C.

The Law of skip Introduction

Prove the following theorem, and bind it to the name SKIP_THM.

!P Q. (!s. (Mb P s) ==> (Mb Q s)) ==> (HOARE P skip Q)

Use SKIP_THM to prove the following goal:

HOARE (%"s" << #1) skip (%"s" << #1)

Hint: Try using MATCH_MP_TAC.

From now on such goals will be shown using the idealised syntax `{s < 1} skip {s < 1}'. You will have to make the translation into the HOL concrete syntax yourself.

Write a tactic called SKIP_TAC that will reduce any goal of the form `{P} skip {Q}' to one of the form `(!s. (Mb P s) ==> (Mb Q s))'.

The Law of ; Introduction

Prove the following theorem (translated into appropriate concrete syntax) and bind it to the name SEQ_THM:

!P Q C₀ C₁. (?R. ({P} C₀ {R}) /\ ({R} C₁ {Q})) ==> ({P} C₀;C₁ {Q})

Use this theorem, together with SKIP_TAC, to prove the following goal:

{s < 1} skip;skip {s < 1}

Write a tactic SEQ_TAC that takes as a parameter a boolean expression valued term R such that SEQ_TAC (Term `R`) is a tactic that will reduce a goal of the form {P} C₀;C₁ {Q} to two simpler subgoals: {P} C₀ {R}, and {R} C₁ {Q}.

The Law of if Introduction

Prove the following theorem (translated into appropriate concrete syntax) and bind it to the name IF_THM:

!P Q B C₀ C₁. ({P & B} C₀ {Q}) /\ ({P & ~B} C₁ {Q}) ==> ({P} if B then C₀ else C₁ {Q})

Write a tactic IF_TAC that will reduce a goal of the form {P} if B then C₀ else C₁ {Q} to two simpler subgoals: {P & B} C₀ {Q}, and {P & ~B} C₁ {Q}.

The Law of := Introduction

The law of := introduction in Hoare logic is expressed in terms of syntactic substitution. Assume that the notation `P[E/v]' means the predicate one gets by syntactically replacing all instances of the variable v with the expression E in the predicate P. The Hoare logic rule for := introduction would then be captured by the following theorem:

!P Q v E. ({P} skip {Q[E/v]}) ==> ({P} v:= E {Q})

The first thing we need to do is to define a syntactic substitution function on boolean expressions.

Substitution

As with the meaning functions Me and Mb, we will need two syntactic substitution functions, one for (numeric) expressions and one for boolean expressions. Define to functions SUBe and SUBb to perform syntactic substitutions on these types of expressions. Your definitions should be such that SUBe E X v will return the expression obtained by syntactically substituting the expression X for all instances of the variable v in the expression E. The function SUBb should work similarly.

Hint: These definitions will both be recursive, and the definition of SUBb will use the function SUBe. Your definitions of Me and Mb should offer you some inspiration.

Our next step is to establish a correspondence between evaluating a substituted expression and evaluating the original expression in an updated state by proving the following theorems, which we shall call SUBe_THM and SUBb_THM respectively:

!E X v s. (Me (SUBe E X v) s) = (Me E (update v (Me X s) s))

!P X v s. (Mb (SUBb P X v) s) = (Mb P (update v (Me X s) s))

Hint: Both these proofs should begin by doing structural induction over the form of expressions and boolean expression respectively. Structural induction is used to prove theorems of the form `!x. P[x]' where x is a variable of some recursive type. For example, SUBe_THM has this form because it begins `!E. ...', where E is a variable of the recursive type expression. Structural induction breaks the proof down into several cases, one for each constructor of the type. In the case of recursive constructors you will able to assume that the property desired holds of the subcomponents while you attempt to prove it holds for the component as a whole.

The tactic to initiate a structural induction in HOL is INDUCT_THEN. This tactic takes two arguments, the first is a theorem which justifies the validity of performing structural induction on the type in question, and the second is another tactic that defines what is done with the inductive hypothesis in the recursive cases. By far the easiest thing to do with the inductive hypotheses is to simply add them to the list of assumptions. As a result, I usually use the tactic as INDUCT_THEN t ASSUME_TAC, where t is the theorem that asserts the validity of induction on the data-type in question.

So, where do you get these theorems about the validity of inducting over a data-type? When you define a recursive data-type HOL returns an axiom that captures the defining property of the type. For example, in the previous exercise set you defined the type of expressions and bound the resulting axiom to he ML value expression_AX. You have already made use of these axioms, when defining recursive functions over a recursive type you need to supply the defining axiom of the type so that HOL can establish the soundness of the definition. For example, you will have used expression_AX when defining the meaning function on expressions Me. Anyway, these defining axioms also imply the validity of performing structural induction over their type, albeit rather indirectly. There is a function supplied in HOL that takes the defining axiom of a type and proves from it a theorem that directly asserts the validity of performing structural induction on that type. This function is called prove_induction_thm. For example, the following code proves the validity of performing structural induction over expressions and binds the resulting theorem to the ML value ex_ind_THM.

val ex_ind_THM = prove_induction_thm expression_AX;

Prove induction theorems for boolean expressions and commands, and bind them to ML values for later use.

Using the induction theorems you now have for expressions and boolean expressions, you should be able to perform the proofs of SUBe_THM and SUBb_THM.

Back to :=

Using the theorems SUBe_THM and SUBb_THM, you should now be able to prove the theorem we originally wanted for := introduction, namely:

!P Q v E. ({P} skip {Q[E/v]}) ==> ({P} v:= E {Q})

Note that the substitution `Q[E/v]' will be need to be written as `SUBb Q E v' when you translate this theorem in to the actual concrete syntax required by HOL.

Using this theorem you can write a tactic for reducing goals about assignment statements.

A Proof

Using the tactics you have defined you should be able to prove that the following code will swap the values of the variables x and y.

t := x; x := y; y := t

Hint: This goal is most easily rendered in HOL as follows:

!X Y. HOARE ((%"x" == #X) && (%"y" == #Y)) ("t" := %"x";; "x" := %"y";; "y" := %"t") ((%"x" == #Y) && (%"y" == #X))