Chapter 1

A Mechanized Hoare Logic of State Transitions

Mike Gordon

The field of programming logics stands on the foundation laid by C.A.R. Hoare in his seminal paper ‘An axiomatic basis for computer programming’ [8]. In that paper Hoare presented a calculus of formulae P{C }Q meaning “If assertion P is true before initiation of a program C , then the assertion Q will be true on its completion.” ^{1} Since 1969, research into Hoare logics has been a major topic in the theory of programming. Numerous variations and extensions of Hoare’s original ideas have been developed. These have both been studied theoretically [1] and put into practice [3, 9]. This tradition is continued here. An interpretation of Hoare logic is described that is intended for the analysis of programs implementing realtime reactive systems. Versions of Hoare’s original rules have been derived and form the basis for a prototype computer assisted program verifier. The aim has been to produce an automated system that uses ‘Hoare-style’ reasoning to establish both total correctness and ‘fine grain’ timing properties of programs. There already exist extensions of Hoare logic that enable the running time of programs to be analysed [11]. The work here extends and automates these. Formulae of the form {P} C {Q} [I ] ⟨t⟩ are introduced where P, Q and I are assertions, C is a command (i.e. a program) and t is a number. These meaning of such formulae is “If P is true and the instructions compiled from C are executed, then in at most t machine cycles the execution of C will terminate in a state satisfying Q and all intermediate states will satisfy I .”

1.1 An introductory example

The simple example given in this section aims to convey the ‘look and feel’ of the verification method presented in subsequent sections. Some notations and concepts appear before they are properly introduced and as a result some of the details may be obscure.

1From now on {P} C {Q} will written instead of Hoare’s original P{C }Q.

2 Mike Gordon

Consider the specification of the form {P} C {Q} [I ] shown in box 1 below. C is an annotated command and P, Q, I are conditions on the values of program variables. The condition I is intended to hold throughout the computation (i.e. in the final state and all intermediate states), whereas Q is only intended to hold in the final state. The annotations in the command are an assertion after the first assignment and a variant [x] and invariant for the while-loop. Each time around the loop the invariant holds and the value of the variant decreases (values are assumed to be positive integers). Variables like x in teletype font are program variables; variables like x in italics are logical variables (also called ‘ghost’ or ‘auxiliary’ variables).

1 {x = x ∧ y = y}

   out := 0; {out = 0 ∧ x = x ∧ y = y}

if ¬(x = 0 ∨ y = 0) then while x > 0

do [x] {out + (x × y) = x × y ∧ y = y}

            out := out + y;
            x := x − 1

{out = x × y }

[y = y]

The verifier initially generates eleven verification conditions. Ten of these are solved by the currently implemented simplifier leaving the following one for the user:

2 (out + (x × y) = x × y) ⇒

   ¬(x = 0) ⇒
   ((out + y) + ((x − 1) × y) = x × y)

This is proved manually and then the verifier generates the theorem shown in box 3 below, which has the form ⊢ {P} C {Q} [I ] ⟨t⟩, where C is the unannotated multiplication program, MultProg say. Such augmented Hoare specifications mean that {P} C {Q} holds (interpreted as a total correctness specification), the execution of C requires at most t cycles and all intermediate states satisfy I .

3 ⊢ {x = x ∧ y = y}

     out := 0;

if ¬(x = 0 ∨ y = 0) then while x > 0 do

              out := out + y;
              x := x − 1

{out = x × y }

[y = y] ⟨15 + (13×x)⟩

A Mechanized Hoare Logic of State Transitions 3

Thus the multiplication takes at most 15 + (13 × x) machine cycles, where x is the initial value of x and the value of program variable y remains stable throughout the computation. This bound on the number of cycles is computed (and verified) automatically. The semantics of {P} C {Q} [I ] ⟨t⟩ is formulated directly in terms of state transitions made by machine instructions compiled from C. The machine MultMachine in box 4 is defined by the sequence of instruction obtained by compiling MultProg (see 1.4). The instruction numbers %n% are comments.

4

MultMachine = Machine [OP0 0; %0 %

                         PUT out;   %1 %
                         GET x;     %2 %
                         OP1 ¬;     %3 %
                         GET y;     %4 %
                         OP1 ¬;     %5 %
                         OP2 ∨;     %6 %
                         OP1 ¬;     %7 %
                         JMZ 22;    %8 %
                         GET x;     %9 %
                         OP0 0;     %10%
                         OP2 >;    %11%
                         JMZ 22;    %12%
                         GET out;   %13%
                         GET y;     %14%
                         OP2 +;    %15%
                         PUT out;   %16%
                         GET x;     %17%
                         OP0 1;     %18%
                         OP2 −;    %19%
                         PUT x;     %20%
                         JMP 9]     %21%

Expanding the theorem of the form {P} C {Q} [I ] ⟨t⟩ into its semantics yields the state transition assertion (or STA) [6] in box 5. State transition assertions are defined in 1.7. They are formulae of the form:

M ⊧ ^{A  \overline{I} \overline{>} B}

which means “If machine M is in a state satisfying A then a state satisfying B will be reached and the sequence of intermediate states will satisfy I.”

In the STA in box 5, vertical stacking means conjunction, At m is true when the program counter is m, [I ] is true of a sequence if I is true of all elements in the sequence and By m is true of any sequence of length less than m.

5

MultMachine ⊧  At 0 x = x y = y \overline{\begin{matrix}By(15 + (13 × x)) \\ [y = y] \end{matrix}} \overline{>} \begin{matrix}At 22 \\ out = x × y \end{matrix}

This says that if control is at instruction number 0 and the values in locations x and y are x and y, respectively, then within 15 + (13 × x) cycles control will reach instruction 22 and the value of out will then be x × y and the value of y will have remained stable throughout the computation. A similar state transition assertion going from instruction n to instruction n + 22 could be deduced if the compiled instructions from MultProg were loaded at position n in memory.

This result is a worst case analysis. If further information is known about the starting state, then a tighter time bound may be provable. For example, in the following annotated specification the precondition has the extra assumption x = 0 and the conditional has been annotated with [F] (which is necessary for the verification condition generator – see 1.6).

6 {x = x ∧ y = y ∧ x = 0}

out := 0; {out = 0 ∧ x = x ∧ y = y ∧ x = 0} if ¬(x = 0 ∨ y = 0) [F] then while x > 0

do [x] {out + (x × y) = x × y ∧ y = y}

            out := out + y;
            x := x − 1

{out = x × y }

[y = y]

The five verification conditions (see 1.6.5) from this are all solved automatically and the resulting STA follows:

7

MultMachine ⊧  At 0 x = x y = y x = 0 \overline{{By 11 \atop [y = y]}} \overline{>} \begin{matrix}At 22 \\ out = x × y \end{matrix}

This shows that if x is initially 0 then the computation takes at most 11 cycles. The STAs in boxes 5 and 7 can be combined into a single STA covering both cases:

8

MultMachine ⊧  At 0 x = x y = y \overline{\begin{matrix}By(x = 0 → 11 | 15 + (13 × x)) \\ [y = y] \end{matrix}} \overline{>} \begin{matrix}At 22 \\ out = x × y \end{matrix}

where b → p | q is the conditional if b then p else q.

1.2 Overview

The verifier illustrated in the previous section is built on top of a version of Hoare logic for judgements of the form {P} C {Q} [I ] ⟨t⟩. This, in turn, is built on top of the theory of state transition assertions and a compiler for a simple programming language. Finally, these are defined directly in higher order logic. Here’s a diagram:

Verification conditions Hoare logic of STAs

Theory of STAs Compiler

Higher order logic

The approach is purely definitional in that each layer is defined in terms of the concepts of a lower one. The theory of STAs and their use in reasoning about machine instructions is described elsewhere [6]. To make this paper self-contained, a simplified version of the theory is outlined in 1.7. The general idea of mechanising Hoare logics by generating verification conditions and then feeding them to a theorem prover is standard [3, 5, 13]. The particular approach used here was originally developed for non-timed Hoare logics [4]. Verification conditions are described in 1.6. The main contribution of this paper is to make the use of STAs for reasoning about data-processing algorithms much easier by defining a Hoare logic on top of them.

1.3 Timed Hoare specifications

The syntax of expressions E and commands C is given by the following BNF, where N ranges over the natural numbers, V ranges over the set Var of program variables, U ranges over unary operators and B ranges over binary operators.

E ::= N | V | U E | E_{1} B E_{2}
C ::= V := E
| C_{1} ; C_{2}
| if E then C
| if E then C_{1} else C_{2}
| while E do C

This BNF syntax is ambiguous; if necessary, brackets will be used to disambiguate particular examples.

Expressions and commands are executed by translating them to sequences of instructions for a simple stack machine and then running the resulting machine code programs. The state of the target machine is a triple (pc, stk, mem) consisting of a program counter pc : ℕ, a stack stk : seq ℕ and a memory mem : Var → ℕ.

The meaning of timed Hoare specifications {P} C {Q} [I ] ⟨t⟩ is defined in terms of the execution of instructions compiled from C.

The specification {P} C {Q} [I ] ⟨t⟩ is true iff ^{2} whenever the program counter points to the beginning of the instructions compiled from C and P is true then the target machine goes through a sequence of states satisfying I and reaches within t steps a state in which Q is true and the program counter points to the end of instructions compiled from C .

This informal definition is refined and formalized in 1.7 using state transition assertions.

2“iff” abbreviates “if and only if”.

1.4 A simple machine and compiler

Programs are compiled to sequences of instructions from the following instruction set:

JMP n unconditional jump to instruction n
JMZ n pop stack then jump to instruction n if the result is zero
JMN n pop stack then jump to instruction n if the result is non-zero
POP  pop the top of the stack
OP0 v push v onto the stack
OP1 U pop one value from stack, perform unary operation U, push result
OP2 B pop two values from stack, perform binary operation B, push result
GET x push the contents of memory location x onto the stack
INP i push the input from i onto the stack
PUT x pop the top of the stack and store the result in memory location x

Let [[E]] denote the instructions that expression E compiles to and let s_{1} ⌢ s_{2} denote the concatenation of sequences s_{1} and s_{2}, then:

[[N]]  = OP0 N
[[V]]  = GET V
[[U E]]  = [[E]] ⌢ OP1 U
[[E_{1} B E_{2}]] = [[E_{1}]] ⌢ [[E_{2}]] ⌢ OP2 B

It is easy to prove that if |E| is the number of instructions in [[E]] then:

\begin{aligned}|N | & = 1 \\ |V| & = 1 \\ |U E| & = |E| + 1 \\ |E_{1} B E_{2}| & = |E_{1}| + |E_{2}| + 1 \end{aligned}

Let [[C]] n be the sequence of instructions that command C compiles to if the first instruction is placed at position n. Let |C| be the number of instructions in [[C]], then:

|V := E|  = |E| + 1
|C_{1} ; C_{2}|  = |C_{1}| + |C_{2}|
|if E then C|  = |E| + |C| + 1
|if E then C_{1} else C_{2}| = |E| + |C_{1}| + |C_{2}| + 2
|while E do C|  = |E| + |C| + 2

and

[[V := E]] n  = [[E]] ⌢ PUT V
[[C_{1} ; C_{2}]] n  = [[C_{1}]] n ⌢ [[C_{2}]](n+|C_{1}|)
[[if E then C]] n  = [[E]] ⌢ JMZ(n+|E|+|C|+1) ⌢ [[C]](n+|E|+1)
[[if E then C_{1} else C_{2}]] n = [[E]] ⌢ JMZ(n+|E|+|C_{1}|+2) ⌢ [[C_{1}]](n+|E|+1)

⌢ JMP(n+|E|+|C_{1}|+|C_{2}|+2) ⌢ [[C_{2}]](n+|E|+|C_{1}|+2)

[[while E do C]] n  = [[E]] ⌢ JMZ(n+|E|+|C|+2) ⌢ [[C]](n+|E|+1) ⌢ JMP n

1.5 A timed Hoare logic

The axioms and rules in this section can all be derived from the definition of {P} C {Q} [I ] ⟨t⟩ given in 1.7 below.

1.5.1 The assignment axiom

The notation P[E/V] denotes the result of substituting E for V in P. The assignment axiom states:

⊢ {P[E/V]} V:=E {P} [P ∨ P[E/V]] ⟨|E| + 1⟩

The assignment takes one more cycle than the evaluation of E and during its execution the value of V is either its initial value or the value of E.

1.5.2 The sequencing rule

\frac{⊢ \{P\} C_{1} \{Q\} [I_{1}] ⟨t_{1}⟩ ⊢ \{Q\} C_{2} \{R\} [I_{2}] ⟨t_{2}⟩}{⊢ \{P\} C_{1}; C_{2} \{R\} [I_{1} ∨ I_{2}] ⟨t_{1} + t_{2}⟩}

The time taken to execute C_{1};C_{2} is the sum of the times taken by C_{1} and C_{2} and throughout the combined computation either I_{1} or I_{2} holds of the memory. The invariant could probably be strengthened to say that first I_{1} and then I_{2} holds; this could be expressed with a ‘chop’ operator from interval temporal logic [10]. So far this strengthening has not been needed and the rule above has been sufficient.

1.5.3 The conditional rules

The one-armed conditional rule is:

\frac{⊢ \{P ∧ E\} C \{Q\} [I ] ⟨t⟩  ⊢ P ∧ ¬E ⇒ Q  ⊢ P ⇒ I}{⊢ \{P\} if E then C \{Q\} [I ] ⟨|E| + t + 1⟩}

The time taken by if E then C is at most the time taken to evaluate E plus the time taken to execute C plus 1. If the invariant I is initially true and its truth is maintained by C, then it is true throughout the entire computation of the conditional.

If it is known that the test E is false, then the time bound can be improved and the invariant strengthened to the precondition (since expression evaluations cannot change the memory).

\frac{⊢ P ⇒ ¬E}{⊢ \{P\} if E then C \{P\} [P] ⟨|E| + 1⟩}

The two-armed conditional rule is:

⊢ {P ∧ E} C_{1} {Q} [I_{1}] ⟨t_{1}⟩
⊢ {P ∧ ¬E} C_{2} {Q} [I_{2}] ⟨t_{2}⟩
⊢ P ∧ E ⇒ I_{1}
⊢ P ∧ ¬E ⇒ I_{2}
⊢ {P} if E then C_{1} else C_{2} {Q} [I_{1} ∨ I_{2}] ⟨|E| + Max(t_{1}, t_{2}) + 2⟩

The time taken to execute if E then C_{1} else C_{2} is at most the time taken to evaluate E plus the maximum of the times taken to execute C_{1} and C_{2} plus 2. If when C_{1} is executed then I_{1} holds throughout the computation and when C_{2} is executed I_{2} holds, then I_{1} ∨ I_{2} holds no matter what arm of the conditional is taken.

If the precondition P determines the value of E, then a tighter time bound can be derived. In the case that P forces E to be true:

\frac{⊢ \{P\} C_{1} \{Q\} [I ] ⟨t⟩  ⊢ P ⇒ E  ⊢ P ⇒ I}{⊢ \{P\} if E then C_{1} else C_{2} \{Q\} [I ] ⟨|E| + t + 2⟩}

In the case that P forces E to be false:

\frac{⊢ \{P\} C_{2} \{Q\} [I ] ⟨t⟩  ⊢ P ⇒ ¬E  ⊢ P ⇒ I}{⊢ \{P\} if E then C_{1} else C_{2} \{Q\} [I ] ⟨|E| + t + 1⟩}

The reason for “2” in the time bound when E is true, but “1” when it is false is that the compiler generates a jump instruction from after the code for C_{1} to the end of the conditional. This jump is not executed if the else-arm is taken.

1.5.4 The while rule

In the rule that follows V is a variant, i.e. a variable whose value strictly decreases each time around the loop; note that all values are natural numbers, so the value of V cannot be negative. The function WhileTime is defined by:

WhileTime(e, t, n) =_{def} e + 1 + n × (e + t + 2)

WhileTime(e, t, n) is an upper bound on the number of cycles taken to execute n iterations of while E do C, where e is an upper bound on the number of cycles to evaluate E and t is an upper bound on the number of cycles to execute C.

\frac{⊢ ∀ v. \{P ∧ E ∧ V = v\} C \{P ∧ V < v\} [I ] ⟨t⟩ ⊢ P ⇒ I}{⊢ ∀ v. \{P ∧ V = v\} while E do C \{P ∧ ¬E\} [I ] ⟨WhileTime(|E|, t, v)⟩}

If it is known that E is false, then the body of the while loop is never executed. This is reflected in the following rule.

\frac{⊢ P ⇒ ¬E}{⊢ \{P\} while E do C \{P\} [P] ⟨|E| + 1⟩}

1.5.5 The consequence rule

Preconditions can be strengthened and postconditions, invariants and time-bounds weakened:

⊢ {P} C {Q} [I ] ⟨t⟩
⊢ P′ ⇒ P
⊢ Q ⇒ Q′
⊢ I ⇒ I′
⊢ t ≤ t′
⊢ {P′} C {Q′} [I′] ⟨t′⟩

1.5.6 The cases rule

⊢ {P_{1}} C {Q} [I ] ⟨t⟩
⊢ {P_{2}} C {Q} [I ] ⟨t⟩
⊢ {P_{1} ∨ P_{2}} C {Q} [I ] ⟨t⟩

1.5.7 An example proof

The following proof establishes the specification in box 6 on page 4. 1. By the assignment axiom:

⊢ {x = x ∧ y = y ∧ x = 0 ∧ 0 = 0}

 out := 0

{x = x ∧ y = y ∧ x = 0 ∧ out = 0} [(x = x ∧ y = y ∧ x = 0 ∧ out = 0) ∨ (x = x ∧ y = y ∧ x = 0 ∧ 0 = 0)] ⟨2⟩

2. By the consequence rule this entails:

⊢ {x = x ∧ y = y ∧ x = 0}

 out := 0

{x = x ∧ y = y ∧ x = 0 ∧ out = 0} [y = y] ⟨2⟩

3. Since (x = x ∧ y = y ∧ x = 0 ∧ out = 0) ⇒ ¬(¬(x = 0 ∨ y = 0)) and |¬(x = 0 ∨ y = 0)| = 8, it follows by the second one-armed conditional rule (the one for when the test is false) that:

⊢ {x = x ∧ y = y ∧ x = 0 ∧ out = 0}

if ¬(x = 0 ∨ y = 0) then C {x = x ∧ y = y ∧ x = 0 ∧ out = 0} [x = x ∧ y = y ∧ x = 0 ∧ out = 0] ⟨9⟩

4. This simplifies by the consequence rule to:

⊢ {x = x ∧ y = y ∧ x = 0 ∧ out = 0}

if ¬(x = 0 ∨ y = 0) then C {out = x × y} [y = y] ⟨9⟩

5. Applying the sequencing rule to 2 and 4 yields:

⊢ {x = x ∧ y = y ∧ x = 0 ∧ out = 0}

  out := 0;

if ¬(x = 0 ∨ y = 0)

   then C

{out = x × y} [y = y] ⟨11⟩

1.6 Verification conditions

The proof in the previous section was a sequence of lines each of which was an axiom or followed from earlier lines by a rule of inference. Such forward proofs are tedious to produce. An alternative is to proceed backwards, by starting from the goal to be proved and then splitting this into subgoals, subsubgoals etc. until instances of axioms are reached. A traditional way of organizing such goal-directed proofs is to use verification conditions [3, 13]. The idea is to generate from a goal {P} C {Q} a set of purely logical formulae – the verifications conditions – that have the property that if they are true then the Hoare specification from which they were generated is also true. To enable verification conditions to be easily generated, the command C needs to be annotated with hints; in particular the variant and invariants for while loops need to be supplied (though attempts have been made to generate this information automatically [14]). The verification conditions are generated by a straightforward recursion on the structure of C.

Verification conditions are related to Dijkstra’s weakest preconditions [2], though they predate it. Dijkstra’s idea was to replace {P} C {Q} by the purely logical formula P ⇒ wp(C, Q), where wp(C, Q) is the weakest precondition for C to establish Q. The rules for calculating P ⇒ wp(C, Q) are similar to the rules for generating verification conditions from {P} C {Q}.

The verifier described here requires the variant and invariant of all while loops to be supplied, as well as an assertion before each command in a sequence that is not an assignment. These assertions should be statements that are true when control reaches the point at which they occur. Additional optional assertions of the form [T] or [F] may also be added after the test in conditional and while commands; these indicate the truth value of the test.

A goal has the form {P} C {Q} [I ], where C is an annotated command. It is assumed that each while command has a distinct variant v (and associated auxiliary variable v) and that for each such variant there is a conjunct v = v in P. The annotations in C enable an expression Time C to be computed syntactically that gives a bound on the running time of C in terms of the initial values of the variants.

Time(V := E)  = |E| + 1
Time(C_{1} ; C_{2})  = Time C_{1} + Time C_{2}
Time(C_{1} ; {R} C_{2})  = Time C_{1} + Time C_{2}
Time(if E then C)  = |E| + Time C + 1
Time(if E [F] then C)  = |E| + 1
Time(if E then C_{1} else C_{2})  = Time E + Max(Time C_{1}, Time C_{2}) + 2
Time(if E [T] then C_{1} else C_{2}) = Time E + Time C_{1} + 2
Time(if E [F] then C_{1} else C_{2}) = Time E + Time C_{2} + 1
Time(while E do [v] {R} C)  = WhileTime (|E|, Time C, v)
Time(while E [F] do [v] {R} C) = |E| + 1

For example, Time(out := out + y; x := x − 1) simplifies to 8 and Time MultProg (where MultProg is the command in box 1 on page 2) simplifies to 15 + (13 × x).

When the verifier is invoked with a goal {P} C {Q} [I ], it tries to prove the specification {P} C {Q} [I ] ⟨Time C⟩ using a set of derived rules ‘backwards’. It matches the specification with the conclusions of these rules (which are given below) and then generates subgoals consisting of the hypotheses of the (unique) rule that matched. ^{3} This process is repeated on the subgoals until they are all reduced to purely logical formulae. These formulae are then mechanically simplified and those that do not reduce to true are returned as the verification conditions. It is clear that if the verification conditions are proved then the rules may be applied in the ‘forward’ direction to establish the original goal. A more detailed discussion of this process can be found elsewhere [4, 5].

The following rules generate the verification conditions; they can be derived from the axioms and rules given in 1.5.

1.6.1 Assignments

\frac{⊢ P ⇒ Q[E/V] Q ∨ Q[E/V] ⇒ I}{⊢ \{P\} V:=E \{Q\} [I ] ⟨Time(V := E)⟩}

1.6.2 Sequencing

\frac{⊢ \{P\} C_{1} \{R\} [I ] ⟨Time C_{1}⟩ ⊢ \{R\} C_{2} \{Q\} [I ] ⟨Time C_{2}⟩}{⊢ \{P\} C_{1}; \{R\} C_{2} \{Q\} [I ] ⟨Time(C_{1} ; C_{2})⟩}

\frac{⊢ \{P\} C \{Q[E/V]\} [I ] ⟨Time C⟩}{⊢ \{P\} C; V := E \{Q\} [I ] ⟨Time(C ; V := E)⟩}

1.6.3 Conditionals

\frac{⊢ \{P ∧ E\} C \{Q\} [I ] ⟨Time C⟩  ⊢ P ∧ ¬E ⇒ Q  ⊢ P ⇒ I}{⊢ \{P\} if E then C \{Q\} [I ] ⟨Time(if E then C)⟩}

\frac{⊢ P ⇒ ¬E  ⊢ P ⇒ Q  ⊢ P ⇒ I}{⊢ \{P\} if E [F] then C \{Q\} [I ] ⟨Time(if E [F] then C)⟩}

3Matching is currently done by an ad hoc procedure which has the definition of Time built in.

A more general approach would use Prolog-style metavariables to synthesize running times by unification. Theorem provers such as Isabelle [12] provide built-in facilities to support this.

⊢ {P ∧ E} C_{1} {Q} [I ] ⟨Time C_{1}⟩ ⊢ {P ∧ ¬E} C_{2} {Q} [I ] ⟨Time C_{2}⟩ ⊢ P ⇒ I

⊢ {P} if E then C_{1} else C_{2} {Q} [I ] ⟨Time(if E then C_{1} else C_{2})⟩

\frac{⊢ \{P ∧ E\} C_{1} \{Q\} [I ] ⟨Time C_{1}⟩  ⊢ P ⇒ E  ⊢ P ⇒ I}{⊢ \{P\} if E [T] then C_{1} else C_{2} \{Q\} [I ] ⟨Time(if E [T] then C_{1} else C_{2})⟩}

\frac{⊢ \{P ∧ ¬E\} C_{2} \{Q\} [I ] ⟨Time C_{2}⟩  ⊢ P ⇒ ¬E  ⊢ P ⇒ I}{⊢ \{P\} if E [F] then C_{1} else C_{2} \{Q\} [I ] ⟨Time(if E [F] then C_{1} else C_{2})⟩}

1.6.4 While loops

⊢ ∀ v. {R(v) ∧ E ∧ v = v} while E do [v] {R(v)} C {R(v) ∧ v < v} [I ] ⟨Time C⟩ ⊢ ∀ v. P(v) ⇒ R(v) ∧ v = v ⊢ ∀ v. R(v) ⇒ I

⊢ ∀ v. {P(v)} while E do [v] {R(v)} C {Q} [I ] ⟨Time(while E do [v] {R(v)} C)⟩

\frac{⊢ P ⇒ ¬E  ⊢ P ⇒ Q  ⊢ P ⇒ I}{⊢ \{P\} while E [F] do [v] \{R\} C \{Q\} [I ] ⟨Time(while E [F] do [v] \{R\} C)⟩}

1.6.5 Example

Consider the goal in box 6 on page 4. Using the definition of Time the verifier computes that 11 cycles are needed. It thus tries to show:

{x = x ∧ y = y ∧ x = 0} out := 0; {out = 0 ∧ x = x ∧ y = y ∧ x = 0} if ¬(x = 0 ∨ y = 0) [F] then while x > 0

do [x] {out + (x × y) = x × y ∧ y = y}

out := out + y;
x := x − 1

{out = x × y } [y = y] ⟨11⟩ Backchaining with the first rule in 1.6.2 yields two subgoals:

(1) {x = x ∧ y = y ∧ x = 0}

 out := 0

{out = 0 ∧ x = x ∧ y = y ∧ x = 0} [y = y] ⟨2⟩

(2) {out = 0 ∧ x = x ∧ y = y ∧ x = 0} if ¬(x = 0 ∨ y = 0) [F] then while x > 0

do [x] {out + (x × y) = x × y ∧ y = y}

          out := out + y;
          x := x − 1

{out = x × y } [y = y] ⟨9⟩

The assignment rule in 1.6.1 reduces (1) to two purely logical verification conditions; both are trivial.

(3) (x = x ∧ y = y ∧ x = 0) ⇒ (0 = 0 ∧ x = x ∧ y = y ∧ x = 0)

(4) (0 = 0 ∧ x = x ∧ y = y ∧ x = 0) ∨ (out = 0 ∧ x = x ∧ y = y ∧ x = 0) ⇒ (y = y)

The second conditional rule 1.6.3 reduces (2) to three purely logical verification conditions; all three are trivial.

(5) (out = 0 ∧ x = x ∧ y = y ∧ x = 0) ⇒ ¬(¬(x = 0 ∨ y = 0))

(6) (out = 0 ∧ x = x ∧ y = y ∧ x = 0) ⇒ (out = x × y)

(7) (out = 0 ∧ x = x ∧ y = y ∧ x = 0) ⇒ (y = y)

The verification conditions from the original goal are (3), (4), (5), (6) and (7). They can all be solved automatically.

1.7 State transition assertions

A state transition assertion (STA) has the form:

M ⊧ ^{A  \overline{I} \overline{>} B}

where M is a machine, A and B are predicates on states and I is a predicate on sequences of states. In general, a machine is a function from states and inputs to states [6], but as inputs are not considered here, a machine will be represented by a function from states to states. If M : state → state is such a machine, then one cycle is a step s ↦ M s. A trace of M is a sequence:

s ⌢ (M s) ⌢ (M(M s)) ⌢ (M(M(M s))) …

The STA above is true iff for all traces s_{0} ⌢ s_{1} ⌢ … of M, if A is true of s_{i} then there is a later state s_{j} (where i < j ) for which B is true and I is true of all subsequences s_{i+1} ⌢ … ⌢ s_{k}, where i < k ≤ j .

A machine code program O determines a machine Machine O that maps a state (pc, stk, mem) to the state resulting from executing the instruction pointed to by the program counter pc. For example, the program in box 4 on page 3 determines a machine that maps the state (8, stk, mem) to the successor state (22, stk, mem), since the program counter (viz. 8) points to the instruction JMP 22 (the program counter starts at 0, so 8 points to the 9th instruction).

The predicate At n is true of a state (pc, stk, mem) iff pc = n. The predicate By t is true of a sequence of states iff its length is at most t.

If the object code for a command C is loaded into program memory starting at location n, then the resulting machine code program, O say, will contain instructions [[C]]n from position n to position n + |C|. The notation Loaded(O, C, n) means that this is the case.

If F is a formula then {F} is the predicate on states defined by:

{F}(pc, stk, mem) = F[mem x_{1}, …, mem x_{n}/x_{1}, …, x_{n}]

where x_{1}, …, x_{n} are the teletype font variables in F and F[v_{1}, …, v_{n}/x_{1}, …, x_{n}] denotes the result of textually substituting v_{i} for x_{i} (for 1 ≤ i ≤ n) in F. For example:

{out + (x × y) = x × y ∧ y = y}(pc, stk, mem) = (mem out) + ((mem x) × (mem y)) = x × y ∧ (mem y) = y

This notation formalizes the convention that teletype font variables are program variables (i.e. names bound by the memory) and italic variables are logical (or auxiliary) variables.

If P is a predicate on states then [P] is the predicate on sequences of states that is true iff P is true of each individual state in the sequence.

The conjunction of predicates on states and sequences of states will be indicated by vertical stacking.

Armed with all this notation, the timed Hoare formula {P} C {Q} [I ] ⟨t⟩ can now be defined to mean:

∀ O n. Loaded(O, C, n) ⇒ Machine O ⊧ \begin{matrix}At n \\ \{P\} \end{matrix} \overline{\begin{matrix}By t \\ [\{I \}] \end{matrix}}\overline{>} \begin{matrix}At(n + |C|) \\ \{Q\} \end{matrix}

In practice, the curley brackets { } are omitted. For example, if O is the sequence of instructions in box 4 on page 3 and Loaded(O, MultProg, 0), then the meaning of the timed Hoare formula in box 3 on page 2 entails the STA in box 5 on page 3.

1.8 Mechanization

The prototype verifier is implemented in HOL [7]. First STAs are defined and various

derived rules for them are proved. Next the stack machine, programming language and compiler are defined. Timed Hoare formulae are then defined in terms of STAs and the various laws in 1.5 are proved. Finally, tactics are programmed to generate verification conditions from goals; the justification part of these tactics are the derived rules [4].

1.9 Conclusions

The work described here is just the beginning of an attempt to provide theorem proving support for specifying and verifying timed reactive systems. Such systems alternate between waiting for input events in the environment and processing the data associated with these events. This paper concentrates on the data processing aspects (another paper [6] discusses waiting states and reaction times). Although some theorem-proving technology has been developed for reasoning about STAs, it is still not clear how useful the STA formalism is as a specification method for ‘real’ real-time systems.

1.10 Acknowledgements

This work was carried out as part of the safemos project; a SERC/DTI funded collaboration between inmos, SRI International, the Oxford University Programming Research Group and the Cambridge University Computer Laboratory. I am grateful to my collaborators on this project: Jonathan Bowen, Juanito Camilleri, Rachel Cardell-Oliver, Roger Hale, John Herbert and David Shepherd. In addition, I have had useful feedback on STAs from Victor Carreno, Nancy Day and Neil Viljoen.

References

[1] Apt, K.R., ‘Ten years of Hoare’s logic: a survey – part 1’, ACM Trans. on Programming Languages and Systems, 3, pp. 431-483, 1981.

[2] Dijkstra, E.W., A Discipline of Programming, Prentice-Hall, 1976.

[3] Good, D.I., ‘Mechanical proofs about computer programs’, in Hoare, C.A.R. and Shepherdson, J.C. (Eds), Mathematical Logic and Programming Languages, Prentice Hall, 1985.

[4] Gordon, M.J.C., ‘Mechanizing Programming Logics in Higher Order Logic’, G. Birtwistle and P.A. Subrahmanyam, (Eds), Current Trends in Hardware Verification and Automated Theorem Proving, Springer-Verlag, 1989.

[5] Gordon, M.J.C., Programming Language Theory and its Implementation, Prentice-Hall International Series in Computer Science, 1988.

[6] Gordon, M.J.C., ‘State transition assertions: a case study’, in Jonathan Bowen (Ed.), Towards System Verification, Real-Time Safety-Critical Systems series, Elsevier, 1993.

[7] Gordon, M.J.C. and Melham, T.F., Introduction to HOL: a theorem-proving environment for higher-order logic, Cambridge University Press, 1993.

[8] Hoare, C.A.R., ‘An axiomatic basis for computer programming’, Communications of the ACM, 12, pp. 576-583, October 1969.

[9] Jones, C.B., Systematic Software Development Using VDM, Prentice Hall, 1986.

[10] J. Halpern, Z. Manna and B. Moszkowski., ‘A Hardware Semantics based on Temporal Intervals’, In the proceedings of the 10-th International Colloquium on Automata, Languages and Programming, Barcelona, Spain, 1983.

[11] Nielson, H.R., ‘A Hoare-like proof system for run-time analysis of programs’, Science of Computer Programming, 9, 1987.

[12] Paulson, L.C., ‘Isabelle: The Next 700 Theorem Provers’, in Odifreddi, P. (Ed) Logic and Computer Science, pp. 361–386, Academic Press, 1990.

[13] von Henke, F.W. and Luckham, ‘Automatic Program Verification III: A Methodology for Verifying Programs’, Stanford University Computer Science Department, Report No. STAN-CS-74-474, 1974.

[14] Wegbreit, B., ‘The synthesis of loop predicates’, Comm. ACM, 17, pp 102–112, 1974.