Towards Verified Systems OVERVIEW

Jonathan Bowen (Ed.)

October 7, 1993 DRAFT CHAPTER BY MJCG

Contents

1 State transition assertions: a case study 3

1.1 An example: Mult . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.1.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.1.2 Informal specification of Mult . . . . . . . . . . . . . . . . . . . . . 5 1.1.3 MultProg: an implementation of Mult . . . . . . . . . . . . . . . . 6

1.2 More detailed specification of Mult . . . . . . . . . . . . . . . . . . . . . . 7 1.3 Determining a machine from a program . . . . . . . . . . . . . . . . . . . . 7 1.4 State transition assertions . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

1.4.1 Holding states . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 1.5 Formal specification of Mult . . . . . . . . . . . . . . . . . . . . . . . . . . 12 1.6 Correctness of MultProg . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 1.7 Generating atomic STAs . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 1.8 Laws for combining STAs . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

1.8.1 The consequence rule . . . . . . . . . . . . . . . . . . . . . . . . . . 17 1.8.2 The sequencing rule . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 1.8.3 Cases rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 1.8.4 The wait loop rule . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 1.8.5 The while rule . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20

1.9 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22

Bibliography 24 2 CONTENTS

Chapter 1

State transition assertions: a case study

M.J.C. Gordon

Overview

The temporal behaviour of programs that interact with their environment depends on the compiler used and the timing characteristics of the host processor. Working out the details can be messy. As part of the safemos project, an approach to managing this complexity based on special-purpose theorem proving tools, has been developed. Specifications are written in a state transition notation annotated with real-time constraints. Implementations are programs coded in a simple imperative language with assignments, sequencing, conditionals, asynchronous inputs, wait-statements, while-commands and forever-loops. The meaning of programs is defined by a translation to sequences of machine instructions, but automated tools can derive behavioural abstractions, called state transition assertions (or STAs) that enable reasoning to be conducted near the source program level.

At the core of the approach are a number of ‘laws’ for combining STAs. These are derived from the definition of state transition assertions and are thus theorems rather than axioms. These laws combine aspects of Hoare logic [4] and interval temporal logic [3]. A specialized theorem prover automatically generates STAs that describe the behaviour of a program considered as a sequence of assignments and jumps (see Section 1.3). Semiautomatic tools then combine these ‘atomic STAs’ to derive STAs for straight line code segments and certain looping structures, including wait loops. Finally, a user interactively combines these derived STAs to establish properties of the candidate implementation.

The machine used in the semantics is idealized: it has an unbounded stack and unspecified word-size. Some mechanized tools have been implemented to enable the actual resources required by a given program to be analysed (e.g. to determine the maximum stack depth). After such an analysis has been carried out, a finite machine customized to the program and suitable for physical realization can be computed. It is intended that such machines will implemented directly in hardware (e.g. with field programmable gate arrays) or via a software emulation; in both cases it is necessary to prove that the abstract machine used as a semantic base is correctly implemented. The physical realization of abstract machines is not considered here.

1.1. An example: Mult

The example program studied here implements a reactive system which is required to meet hard real-time constraints. It is also required to be resettable from an arbitrary processor state within a hard real-time bound; this is intended to support fault recovery protocols. The approach adopted is to count the number of machine cycles taken by the compiled code. This very fine-grained kind of analysis may be quite inappropriate in some situations; intended applications include low-level communication software, critical systems requiring very rapid responses and the software emulation of hardware functions. The example in this chapter illustrates aspects of all of these.

Programs use a very simple low-level input/output model. Inputs are ‘asynchronously’ supplied by the environment, outputs are ‘memory mapped’. When an input is read, the program gets whatever value the environment happens to be offering at the time of the read. For example, inputs might be provided directly by a sensor. It is assumed inputs are digitized, but not that they are latched. Outputs, on the other hand, are identified with particular program variables whose values are assumed to remain stable until changed. Thus outputs are latched. This particular treatment of input/output was chosen for two reasons: it corresponds to a simple physical implementation and it can be used to model more complex regimes. For example, a regime in which inputs are latched would be modeled by requiring the environment to hold inputs stable between input events. The example in this chapter may be viewed as a study of the fine detail underlying a particular kind of synchronized communication. Juanito Camilleri has studied this topic more generally, with the eventual aim of producing a verified implementation of occamstyle synchronized communication in terms of the simple input/output model described here [1].

1.1.1. Overview

Mult is a multiplier that reacts with the environment via a four-phase handshake. The first phase is a request by the environment that two numbers be read from input lines; the second phase is the reading of these by the program; the third phase is the initiation, by the environment, of the multiplication of the two numbers read in during the second phase; the fourth phase is the computation of the product. At the end of such a cycle the program outputs the computed product whilst awaiting the first phase of a new cycle. The first three phases all take place within a fixed time bound; the duration of the fourth phase depends on the size of the numbers being multiplied.

1.1.2. Informal specification of Mult

Mult has two data inputs in1 and in2 that carry numbers.^{1} It has two control inputs req and reset that carry truthvalues (i.e. single bits). It has one numerical data output out and one boolean^{2} control output avail.

In the normal operation of Mult there are just four possibilities, corresponding to the four phases of the handshake: (i) it is waiting to engage in a handshake; (ii) it is reading inputs; (iii) it is waiting to start a multiplication; (iv) it is performing a multiplication. Both (i) and (iii) are ‘wait states’: the waiting will continue indefinitely until the environment sends the appropriate signal via the req input (see below). The other possibilities, (ii) and (iv), are transitions between waiting states.

It is required that no matter what state the host processor is in, if the environment holds reset at the value 1 continuously for δ_{1} cycles, then the system Mult will be reset to the state (i) of waiting to engage in a handshake. In this state the value output on

avail is 1.

The environment signals the start of a handhake by changing the input req from 0 to 1. When this happens, it is required that the system will input the values, m and n say, on inputs in1 and in2 and move to a state in which it is waiting to start the multiplication of m and n. This inputting transition is required to complete within δ_{2} processor cycles. The system will then wait, outputting 0 on avail, until the environment sets the input req to 0. When that happens the system will compute m × n, output this value on out, and then return to the initial state. This multiplication transition is required to take place within δ_{3}(m) cycles. The timing parameters δ_{1} and δ_{2} are given numbers and δ_{3} is a given function.

This specification requires that if Mult is waiting to engage in a handshake, then the product m ×n can be computed in δ_{2} +δ +δ_{3}(m) machine cycles, where δ is the number of machine cycles taken by the environment to set req to 0 after m and n have been input. But how can the environment know when Mult is in the state of waiting to engage in a handshake? It is specified that in this state avail has value 1, but the converse is not necessarily the case. For example, the value of avail will continue to be 1 for a short time after the environment sets req to 1, i.e. during the first part of phase (ii) of the handshake. It is tempting to require in the specification that avail be 1 if and only if the system is waiting to engage in a handshake, but such a specification would be unimplementable. This is because there will always be time delays in sensing environmental changes and then communicating the results to outputs, hence there will always be times at which internal state changes have occurred, but not yet been signalled on outputs. In general, when timing is considered, it is not possible to characterize internal states by instantaneous values on outputs. However, if inputs and outputs are observed over a sequence of cycles, then conclusions about internal states can be drawn. For example, if the input reset has been 1 for δ_{1} cycles, then the specification requires the system to be waiting to engage in a handshake.

1For simplicity, arbitrary-precision (i.e. ‘mathematical’) numbers are used here but, at the expense of some arithmetical messiness, finite-precision numbers could have been used instead.

2The truthvalues T and F will be represented by the numbers 1 and 0, respectively, because the programming language used only supports one data type: the natural numbers ℕ.

1.1.3. MultProg: an implementation of Mult Here is a program that implements Mult.

   0:    MultProg =
   1:     FOREVER
   2:      avail := 1;
   3:      IF INPUT req
   4:       THEN avail := 0;
   5:            x := INPUT in1;
   6:            y := INPUT in2;
   7:            AWAIT[NOT(INPUT req); INPUT reset];
   8:            out := 0;
   9:            IF (x=0) OR (y=0)
   10:            THEN  SKIP
   11:            ELSE  WHILE (x > 0) AND NOT(INPUT reset)
   12:                   DO out := out + y;
   13:                      x   := x - 1
   14:                   OD
   15:         avail := 1
   16:      ELSE  SKIP

The command FOREVER C is an abbreviation for WHILE TRUE DO C . The command AWAIT[E_{1}; …; E_{n}] loops until one of E_{1}, …, E_{n} becomes true (i.e. has the value 1) and then control moves to the next command. Evaluating an expression INPUT i reads the current value offered by the environment at input i and returns the result. Outputs are identified with program variables, so are set by assignment. The other constructs in MultProg should be self-explanatory.

Note that there is some arbitrariness in the placement of assignments. The occurrence of avail:=1 on line 2 could be moved to before the FOREVER-loop. The assignment avail:=0 is performed before the inputs in1 and in2 are read, however the specification only requires avail to be 0 when Mult is waiting to start the multiplication. The verification given here also works if avail:=0 is performed after the two reads, or even between them (perhaps this indicates that the specification is inadequate: maybe it should be required that the inputs remain stable only as long as avail is 1).

MultProg works as follows: initially it is waiting to engage in a handshake by looping between lines 2, 3 and 16 in the outer FOREVER-loop. If the input req is 1 then eventually the test at line 3 will be reached and then lines 4, 5 and 6 will be executed in sequence resulting in avail being set to 0 and the values at inputs in1 and in2 being read into the variables x and y, respectively. The program will then loop at the AWAIT-command at line 7. If either req is 0 or reset is 1 this command will terminate, control will move to line 8 and the multiplication will begin with out being initialized to 0. If either of the two numbers to be multiplied are 0, then nothing needs to be done (line 10), avail is set back to 1 (line 15) and the system is ready again to engage in a handshake. However, if either of x or y is non-zero, then the product is computed in out by repeatedly adding y to out (lines 11—14). Note that each time around this WHILE-loop, reset is tested and if found to be 1 the loop is terminated. Once the loop is terminated, which (in the absence of a 1 at reset) will be in a time proportional to the value read into x, avail is set to 1 (line 15) and control returns to the outer loop (lines 2, 3, and 16) and the system is ready to engage in another handshake, i.e. is back in phase (i).

It is clear by inspection, that if reset is held at 1 for sufficiently long then control will eventually move to the outer FOREVER-loop. This is because all loops test reset.

1.2. More detailed specification of Mult

The view of real-time systems taken here is that they are sequential machines. A specification places requirements on the behaviour of a machine and an implementation is an actual machine that meets these requirements. The reason for this rather concrete approach is to try to minimize the gap between abstract models of behaviour and real machines. The device that ultimately runs programs implements a sequential machine, so it helps tie the hardware and software verifications together if they both use the same kind of behavioural model.

A machine is a function M : inputs → (state → state). M should be thought of as an instruction processor: if the environment offers an array of inputs ι and the current state is σ, then executing the next instruction results in the state M ι σ . The state will include a program counter and a memory that associates state variables with data values. This memory is a function from names to values (i.e. numbers). Inputs too are modelled by functions from names to values. It is assumed that at each moment the environment specifies a value ι i for each input i, i.e. it determines a mapping ι : name → ℕ, that varies with time. For any particular system there will only be a small finite number of inputs (in1, in2, req and reset for Mult), but this fact does not need to be builtin to the general theory. It will be assumed that some state variables are readable by the environment (avail and out for Mult). During each cycle of execution of M, an instruction is selected and executed, resulting in a new state. If the instruction is an input, then this new state will depend on the inputs supplied by the environment.

In what follows, it is first shown how the program MultProg in Section 1.1.3 determines a machine and then how the informal specification Mult in Section 1.1.2 can be expressed as a predicate on machines. Finally, a method is outlined for proving that programs meet specifications and it is illustrated using MultProg and Mult.

1.3. Determining a machine from a program

It is straightforward to define a function that recursively translates a program to a sequence of assignments and conditional jumps. For example, one particular algorithm translates MultProg to:

  0:    avail := 1
  1:    IF INPUT req THEN SKIP ELSE GOTO 18
  2:    avail := 0
  3:    x := INPUT in1
  4:    y := INPUT in2
  5:    IF NOT(INPUT req) THEN SKIP ELSE GOTO 7
  6:    GOTO 10
  7:    IF INPUT reset THEN SKIP ELSE GOTO 9
  8:    GOTO 10
  9:    GOTO 5
  10:   out := 0
  11:   IF NOT x OR NOT y THEN SKIP ELSE GOTO 13
  12:   GOTO 17
  13:   IF x > 0 AND NOT(INPUT reset) THEN SKIP ELSE GOTO 17
  14:   out := out + y
  15:   x := x - 1
  16:   GOTO 13
  17:   avail := 1
  18:   GOTO 0

Assignments and conditional jumps require the evaluation of an expression, which may be arbitrarily large, and thus take an arbitrary amount of time to evaluate. It is thus not immediately clear how a sequence of assignments or jumps can be directly represented by a machine. Another tricky issue concerns input. Consider the conditional jump on line 13: the exact time at which reset is read depends on how the expression

x > 0 AND NOT(INPUT reset) is evaluated.

To specify the detailed semantics of expression evaluation, programs will be further translated to sequences of instructions for a simple stack machine with 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 op_{1} pop one value from stack, perform unary operation op_{1}, push result
OP2 op_{2} pop two values from stack, perform binary operation op_{2}, 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

It is straightforward to define a translation of assignments and jumps to sequences of machine instructions. For example, the conditional jump at line 13 is translated to the following sequence of stack machine instructions:

   GET x
   OP0 0
   OP2 >
   INP reset
   OP1 NOT
   OP2 AND
   JMZ ...

It will be assumed that the operations >, NOT and AND can be performed in one machine cycle, thus the stack machine code determines that x > 0 AND NOT(INPUT reset) takes 7 cycles, and the input occurs on the 4th cycle.

The state of the stack machine is a triple (pc, stk, mem) consisting of a program counter pc : ℕ, a stack stk : seq ℕ and a memory mem : name → ℕ. The model given here does not specify an upper bound on the length of the stack or size of data. Of course, real machines are finite so any actual implementation will have a bounded stack and a particular word size. The intension is to provide tools that ‘fit’ a given program into a finite refinement of the machine; this will not be discussed in detail here (though see the example state transition assertion in Section 1.4).

The semantics of the instructions of the stack machine is defined by a function Step. Before defining Step, some auxiliary notation is required. A conditional ‘if b then e_{1} else e_{2}’ will be written as (b → e_{1} | e_{2}). The empty sequence is denoted by ⟨ ⟩, ⟨x⟩ denotes the sequence with one member, x and ⟨x_{1}, x_{2}, …, x_{n}⟩ denotes the sequence (of length n) containing x_{1}, x_{2}, …, x_{n}. The length of a sequence s is denoted by #s. The nth element of a sequence s will be denoted by s n and the tail of s will be denoted by †s. The tail of ⟨ ⟩ is defined to be ⟨ ⟩ (sequences will be used to represent stacks and the stack manipulating instructions are specified so that popping an empty stack leaves an empty stack). The concatenation of sequences s_{1} and s_{2} will be denoted by s_{1} ⌢ s_{2}. Note that the result of ‘consing’ x onto a sequence s is ⟨x⟩ ⌢ s. If mem is a function representing a memory (i.e. a function from names to values), then Store v x mem denotes the memory identical to mem except on argument x, which it maps to v, i.e. the memory updated with value v at x.

The function Step can now be defined. Its type is:

Step : instruction → (inputs → state → state)

where:

inputs  = name → ℕ
state  = program−counter × stack × memory
program−counter = ℕ
stack  = seq ℕ
memory  = name → ℕ

Step is defined by:

Step (JMP n) ι (pc, stk, mem) = (n, stk, mem)
Step (JMZ n) ι (pc, stk, mem) = ((stk 1 = 0 → n | pc+1), †stk, mem)
Step (JMN n) ι (pc, stk, mem) = ((stk 1 = 1 → n | pc+1), †stk, mem))
Step (POP) ι (pc, stk, mem)  = (pc+1, †stk, mem)
Step (OP0 v) ι (pc, stk, mem) = (pc+1, ⟨v⟩ ⌢ stk, mem)
Step (OP1 op_{1}) ι (pc, stk, mem) = (pc+1, ⟨op_{1}(stk 1)⟩ ⌢ †stk, mem)
Step (OP2 op_{2}) ι (pc, stk, mem) = (pc+1, ⟨op_{2}(stk 2, stk 1)⟩ ⌢ ††stk, mem)
Step (GET x) ι (pc, stk, mem) = (pc+1, ⟨mem x⟩ ⌢ stk, mem)
Step (INP i) ι (pc, stk, mem) = (pc+1, ⟨ι i⟩ ⌢ stk, mem)
Step (PUT x) ι (pc, stk, mem) = (pc+1, †stk, Store (stk 1) x mem)

The machine Machine instrs determined by a sequence of instructions instrs is defined by:

Machine instrs ι (pc, stk, mem) =

(pc < #instrs → Step (instrs(pc+1)) ι (pc, stk, mem) | (0, stk, mem))

The reason for pc+1 is because the program counter starts at 0 not 1. Note that if the program counter pc points outside the program (i.e. pc ≥ #instrs) then the machine jumps to 0.

If P is a program, let Compile P denote the translation of P to stack machine instructions; this is the composition of the translation to assignments and jumps with the translation of these to machine instructions. The machine determined by P is thus Machine(Compile P). For example, the machine corresponding to MultProg is denoted by Machine(Compile MultProg); this will be called MultMachine.

1.4. State transition assertions

Specifications are formalized as predicates on machines. The informal specification of Mult given in Section 1.1 involved a number of transitions between wait states. These can be represented using a kind of assertion, called a state transition assertion (or STA), that combines aspects of the ‘leads-to’ and ‘until’ operators of temporal logic and also resembles a state delta [5]. The general form of an STA is:

M ⊧ A \overline{{Q \atop P}} \overline{>} B

where:

• M : inputs → state → state is a machine;

• A : state → 𝔹 is called the state precondition;

• B : state → 𝔹 is called the state postcondition;

• P : seq inputs → 𝔹 is called the input precondition;

• Q : seq state → 𝔹 is called the output postcondition.

The intuition behind state transition assertions is straightforward: if M is in a state satisfying A and a sequence of inputs arrives that satisfies P, then a state satisfying B will be reached and the sequence of intermediate states will satisfy Q. The formal definition is slightly delicate as it has to cover the possibility that inputs start to arrive satisfying P, but then stop satisfying it before a state satisfying B is reached. A trace of machine M is an infinite sequence ⟨(ι_{0}, σ_{0}), (ι_{1}, σ_{1}), …, (ι_{n}, σ_{n}), …⟩ such that σ_{m+1} = M ι_{m} σ_{m} for all m. It is an A-trace iff A σ_{0}. Observe that the state entered by M after a sequence ι_{0}, …, ι_{n} of inputs have arrived is σ_{n+1}. Thus the machine generates the sequence ⟨σ_{1}, …, σ_{n}, σ_{n+1}⟩ of states from the inputs ι_{0}, …, ι_{n}. With this observation in mind, the following auxiliary concepts are defined.

• B succeeds at n in trace ⟨(ι_{0}, σ_{0}), (ι_{1}, σ_{1}), …, (ι_{n}, σ_{n}), …⟩ iff B σ_{n+1}.

• P fails at n in trace ⟨(ι_{0}, σ_{0}), (ι_{1}, σ_{1}), …, (ι_{n}, σ_{n}), …⟩ iff ¬P⟨ι_{0}, …, ι_{n}⟩.

• Q holds until n in trace ⟨(ι_{0}, σ_{0}), (ι_{1}, σ_{1}), …, (ι_{n}, σ_{n}), …⟩ iff Q⟨σ_{1}, …, σ_{m}⟩ for all m such that 1 ≤ m ≤ n+1.

The state transition assertion:

M ⊧ A \overline{{Q \atop P}} \overline{>} B

holds iff for every A-trace τ of M there exists an n such that (i) either B succeeds at n in τ or P fails at n in τ and (ii) Q holds until the first such n in τ.

An example of a state transition assertion is shown below using a number of notational conventions that are explained immediately afterwards. It is true of a machine M if whenever the predicate Available is true and the variables x, y, z have the values x, y, z respectively, then as long as the reset line keeps at 0, a sequence of steps of length less than δ x will be traversed in which y remains stable with value y, Available is false and the length of the stack is less than d. Furthermore, the sequence ends in a state in which Available is false, x is 0, y is y and z is x × y.

M ⊧ Available ; x ≡ x ; y ≡ y ; z ≡ z \overline{By(δ x) [ \begin{matrix}y ≡ y \\ ¬Available \\ StackMax d \end{matrix} ] [reset ≡ 0]}\overline{>} ¬Available ; x ≡ 0 ; y ≡ y ; z ≡ x × y

Vertical stacking means conjunction. The notation v ≡ x (where v is a name and x a value) is overloaded; it is used both for predicates on states and for predicates on inputs:

(v ≡ x)(pc, stk, mem) =_{def} mem(v) = x
(v ≡ x)ι  =_{def} ι(v) = x

StackMax m is true of a state if the length of the stack is less than m.

StackMax m (pc, stk, mem) =_{def} #stk ≤ m

If μ is either a state or an input, M is either a predicate on states or a predicate on inputs, then:

(¬M ) μ  =_{def} ¬(M μ)
[M ]⟨μ_{1}, …, μ_{n}⟩  =_{def} M μ_{1} ∧ … ∧ M μ_{n}
(By m)⟨μ_{1}, …, μ_{n}⟩ =_{def} n ≤ m

The notation [M ] asserts that M holds at all points in a sequence, so it is analogous to the modal formula □M . As a mnemonic, think of sawing the box operator □ in two and writing the first half before M and the other half after M .

1.4.1. Holding states

Part of the specification of Mult is that it remain waiting to engage in a handshake as long as the request line req is 0. If ‘waiting to engage in a handshake’ is represented by the predicate Available, then this part of the specification can be represented by:

Mult ⊧ Available \overline{\begin{matrix}By 1 \\ [req ≡ 0] \end{matrix}}\overline{>} Available

which will be abbreviated to:

Mult ⊧ req ≡ 0 Holds Available

notice that “By 1” means “1 host machine cycle” not “1 program step” (whatever that might mean).

Whilst Mult is waiting to engage in a handshake it should be outputting the result of the previous handshake on out and outputting 1 on avail. Therefore in the actual specification given in Section 1.5, instead of the predicate Available, a parameterized predicate Ready z is used, with the interpretation “ready to engage in a handshake whilst outputting z on out and 1 on avail”. In general, waiting states are characterized by a parameterized predicate (e.g. Ready z, see Section 1.8.4), an invariant (e.g. avail ≡ 1 and out ≡ z) and a holding condition (e.g. req ≡ 0). In the diagram representing the formal specification of Mult, the existence of such a waiting state is represented graphically by:

Ready z

                                       avail ≡ 1 ; out ≡ z

                                        req ≡ 0

This abbreviates the conjunction of an STA representing the holding condition and a formula expressing the invariant (which uses the logical operators ∧ and ⟹ which are explained below).

Mult ⊧ req ≡ 0 Holds (Ready z) ∧ Ready z ⟹ avail ≡ 1 ∧ out ≡ z

where, letting μ range over states or inputs as before:

(M_{1} ∧ M_{2}) μ =_{def} (M_{1} μ) ∧ (M_{2} μ)
(M_{1} ⟹ M_{2}) =_{def} ∀ μ . (M_{1} μ) ⇒ (M_{2} μ)

Other similar notation used later includes:

True μ  =_{def} T
(M_{1} ⇒ M_{2}) μ  =_{def} M_{1} μ ⇒ M_{2} μ
(M_{1} ∨ M_{2}) μ  =_{def} M_{1} μ ∨ M_{2} μ
(∃x. M x) μ  =_{def} ∃ x. (M x) μ
(P_{1} ∧ P_{2})⟨μ_{1}, …, μ_{n}⟩ =_{def} P_{1}⟨μ_{1}, …, μ_{n}⟩ ∧ P_{2}⟨μ_{1}, …, μ_{n}⟩
(P_{1} ∨ P_{2})⟨μ_{1}, …, μ_{n}⟩ =_{def} P_{1}⟨μ_{1}, …, μ_{n}⟩ ∨ P_{2}⟨μ_{1}, …, μ_{n}⟩

Notice that there are three different kinds of implication: ordinary logical implication ⇒ and two relations between predicates ⇒ and ⟹. The relations between predicates are connected by M_{1} ⟹ M_{2} = ∀ μ . (M_{1} ⇒ M_{2}) μ.

1.5. Formal specification of Mult

A program implementing Mult must be able to cycle within two sets of states representing waiting to engage in a handshake and waiting to start a multiplication. Thus the formal specification asserts the existence of two predicates representing these sets of states. In addition, an implementation must support various invariants and transitions, which can be expressed using STAs. The complete specification can be represented by the following diagram, which represents a conjunction of STAs (details below).

True

\begin{matrix}By δ_{1} \\ [reset ≡ 1] \end{matrix}

>

Ready z

                   avail ≡ 1 ; out ≡ z

                    req ≡ 0

\begin{matrix}By δ_{2} \\ [out ≡ z] \end{matrix}

                              [ \begin{matrix}req ≡ 1 \\ reset ≡ 0 \\ in1 ≡ x \\ in2 ≡ y \end{matrix} ]

>

Ack x y z

                                               avail ≡ 0 ; x ≡ x ; y ≡ y ; out ≡ z

                                                req ≡ 1

By(δ_{3} x)

                                                          [ \begin{matrix}req ≡ 0 \\ reset ≡ 0 \end{matrix} ]

>

Ready(x × y)

                                                                          avail ≡ 1 ; out ≡ x × y

                                                                            req ≡ 0

The predicate Ready z is true of states that are passed through whilst waiting to engage in a handshake. During this waiting, out has value z. The predicate Ack x y z is true of states that are passed through whilst waiting to start a multiplication. During this waiting x, y, z have the values x, y, z, respectively. This diagram defines a predicate MultSpec(δ_{1}, δ_{2}, δ_{3}) on machines M by the following formula (the abbreviations Reset, ReadyInv, ReadyHold, ReadyToAck, AckInv, AckHold, AckToReady are explained later).

MultSpec (δ_{1}, δ_{2}, δ_{3}) M = ∃ Ready Ack.

(M ⊧ Reset(δ_{1}, Ready))  ∧
(∀ z. ReadyInv(Ready, z))  ∧
(∀ z. M ⊧ ReadyHold(Ready, z))  ∧
(∀ x y z. M ⊧ ReadyToAck(δ_{2}, Ready, Ack, x, y, z)) ∧
(∀ x y z. AckInv(Ack, x, y, z))  ∧
(∀ x y z. M ⊧ AckHold(Ack, x, y, z))  ∧

(∀ x y z. M ⊧ AckToReady(δ_{3}, Ready, Ack, x, y, z))

The reset condition Reset(δ_{1}, Ready) asserts that if reset is held equal to 1 for at least δ_{1} then the system will be in a state satisfying Ready z, for some z.

Reset(δ^{1}, Ready) =^{def} True \overline{\begin{matrix}By δ_{1} \\ [reset ≡ 1] \end{matrix}}\overline{>} ∃z. Ready z

States satisfying Ready z should output 1 on avail and z on out.

ReadyInv(Ready, z) =_{def} Ready z ⟹ avail ≡ 1 ∧ out ≡ z

States continue to satisfy Ready z as long as req is 0.

ReadyHold(Ready, z) =_{def} req ≡ 0 Holds (Ready z)

If the system is in a state satisfying Ready z and for at least δ_{2} cycles req is held at 1, reset at 0, in1 at x and in2 at y, then the system will be in a state satisfying Ack x y z.

ReadyToAck(δ_{2}, Ready, Ack, x, y, z) =_{def} Ready z \overline{By δ_{2} [ \begin{matrix}req ≡ 1 ∧ reset ≡ 0 \\ in1 ≡ x ∧ in2 ≡ y \end{matrix} ]}\overline{>} Ack x y z

States satisfying Ack x y z should output 0 on avail and x, y, z on x, y, out, respectively.

AckInv(Ack, x, y, z) =_{def} Ack x y z ⟹ avail ≡ 0 ∧ x ≡ x ∧ y ≡ y ∧ out ≡ z

States continue to satisfy Ack x y z as long as req is 1 and reset is 0.

AckHold(Ack, x, y, z) =_{def} (req ≡ 1 ∧ reset ≡ 0) Holds (Ack x y z)

If the system is in a state satisfying Ack x y z and then for at least δ_{3} x, req is held at 0 and reset at 0 then the system will be in a state satisfying Ready(x×y).

AckToReady(δ^{3}, Ready, Ack, x, y, z) =^{def} Ack x y z \overline{By(δ_{3} x) [req ≡ 0 ∧ reset ≡ 0]}\overline{>} Ready(x×y)

1.6. Correctness of MultProg

The program MultProg is correct if the machine, MultMachine, that it defines satisfies the predicate MultSpec(δ_{1}, δ_{2}, δ_{3}). In fact, it follows that:

MultSpec (43, 13, λ x. 30 + (15 × x)) MultMachine

which establishes correctness with the timing parameters δ_{1} = 43, δ_{2} = 13 and the function δ_{3} defined by δ_{3} x = 30 + (15 × x).

The rest of this chapter is devoted to outlining how such correctness results can be proved. Mechanized theorem proving tools are used since there is a large amount of detail in even small examples.^{3}

1.7. Generating atomic STAs

The program is translated to a sequence of intermediate commands that are either assignments or jumps and then two STAs are generated for each intermediate command. The first of these describes transitions from the beginning of a comand to its end; the second describes transitions from anywhere inside the command to its end. Before explaining this the formalization of “beginning”, “inside” and “end” must be given.

Figure 1.1 shows both the intermediate commands and the final machine instructions for MultProg. Consider the intermediate command with number 13: the beginning of this is the machine instruction numbered 27 (i.e. GET x) and the end of it is after the machine instruction numbered 33 (i.e. JMP 42). The execution of MultProg is said to be inside intermediate command number 13 if it is executing a machine instruction whose number is in the set {27, 28, 29, 30, 31, 32, 33}. Both intermediate commands and machine instructions will be indexed by their position. A program P defines, via the compiler, a mapping Positions(P) from command numbers to instruction numbers in which each command number is mapped to the number of its first instruction. For example, Positions(MultProg) is the following mapping.

3383,547 primitive inference steps were performed, mostly automatically, to verify MultProg.

1.7. GENERATING ATOMIC STAS 15

0:  avail := 1 ............................................ 0:  OP0 1
1:  PUT avail
1:  IF INPUT req THEN SKIP ELSE GOTO 18 ................... 2:  INP req
3:  JMZ 44
2:  avail := 0 ............................................ 4:  OP0 0
5:  PUT avail
3:  x := INPUT in1 ........................................ 6:  INP in1
7:  PUT x
4:  y := INPUT in2 ........................................ 8:  INP in2
9:  PUT y
5:  IF NOT(INPUT req) THEN SKIP ELSE GOTO 7 ............... 10: INP req
11: OP1 NOT
12: JMZ 14
6:  GOTO 10 ............................................... 13: JMP 18
7:  IF INPUT reset THEN SKIP ELSE GOTO 9 .................. 14: INP reset
15: JMZ 17
8:  GOTO 10 ............................................... 16: JMP 18
9:  GOTO 5 ................................................ 17: JMP 10
10: out := 0 .............................................. 18: OP0 0
19: PUT out
11: IF NOT x OR NOT y THEN SKIP ELSE GOTO 13 .............. 20: GET x
21: OP1 NOT
22: GET y
23: OP1 NOT
24: OP2 OR
25: JMZ 27
12: GOTO 17 ............................................... 26: JMP 42
13: IF x > 0 AND NOT(INPUT reset) THEN SKIP ELSE GOTO 17 .. 27: GET x
28: OP0 0
29: OP2 >
30: INP reset
31: OP1 NOT
32: OP2 AND
33: JMZ 42
14: out := out + y ........................................ 34: GET out
35: GET y
36: OP2 +
37: PUT out
15: x := x - 1 ............................................ 38: GET x
39: OP1 pre
40: PUT x
16: GOTO 13 ............................................... 41: JMP27
17: avail := 1 ............................................ 42: OP0 1
43: PUT avail
18: GOTO 0 ................................................ 44: JMP 0

Figure 1.1. Intermediate commands and machine instructions for MultProg

{0 ↦ 0,  1 ↦ 2,  2 ↦ 4,  3 ↦ 6,  4 ↦ 8,  5 ↦ 10, 6 ↦ 13,
7 ↦ 14, 8 ↦ 16, 9 ↦ 17, 10 ↦ 18, 11 ↦ 20, 12 ↦ 26, 13 ↦ 27,
14 ↦ 34, 15 ↦ 38, 16 ↦ 41, 17 ↦ 42, 18 ↦ 44}

Recall that the state of the stack machine is a triple (pc, stk, mem) consisting of a program counter pc : ℕ, a stack stk : seq ℕ and a memory mem : name → ℕ. Define:

At(P) n (pc, stk, mem) = (pc = Positions(P)(n)) In(P) n (pc, stk, mem) = (Positions(P)(n) ≤ pc < Positions(P)(n + 1)) .

Then At(P)n is the predicate on states that is true of σ iff σ is at the beginning of the intermediate command numbered n in program P and In(P)n is the predicate on states that is true of σ iff σ is inside command n.

Consider a program P containing an assignment at position n_{2}:

     :

n_{1}: …

   n_{2}:  x := ((INPUT in) + y)

n_{3}: …

     :

Given a list of significant state variables (e.g. x, y and z), the STA generator will automatically deduce two STAs for the command at n_{2}:

Machine(Compile P) ⊧ At(P) n_{2} ; x ≡ x ; y ≡ y ; z ≡ z \overline{By 4 [ \begin{matrix}In(P) n_{2} \\ y ≡ y \\ z ≡ z \end{matrix} ] [in ≡ in]}\overline{>} At(P) n_{3} ; x ≡ in+y ; y ≡ y ; z ≡ z

Machine(Compile P) ⊧ In(P) n_{2} ; x ≡ x ; y ≡ y ; z ≡ z \overline{By 4 [ \begin{matrix}In(P) n_{2} \\ y ≡ y \\ z ≡ z \end{matrix} ] True}\overline{>} \begin{matrix}At(P) n_{3} \\ y ≡ y \\ z ≡ z \end{matrix}

The first of these asserts that if the input in is held stable with value in, then there is a transition taking at most four cycles from the beginning of the comand at n_{2} to the beginning of the command at n_{3}. During this transition only states in n_{2} are passed through and the values of y and z are unchanged, but the value of x changes to in+y, where y is the value of the variable y.

The second of these asserts that under arbitary input conditions, there is a transition from anywhere in n_{2} to the begining of n_{3}. This transition takes at most four cycles, only passes through states in n_{2} and doesn’t change the values of x and y.

The implemented tool also automatically proves that the stack will grow by at most two during the transition, but because this feature is not used in the Mult example the details are not discussed here.

The first stage in verifying MultProg is to generate two STAs for each of the nineteen intermediate commands. The result of this will not be shown here due to lack of space. Note, however, that users of the verification tool are not expected to have to study these atomic STAs in detail; they are fed into other tools that derive higher level results. These tools combine the atomic STAs using various derived laws.

1.8. Laws for combining STAs

Some of the laws for combining STAs are analogous to rules of Hoare logic. In what follows P, Q etc. will range over predicates on sequences, p, q etc. will range over predicates on the elements of sequences and A, B etc. will range over predicates on states.

Each law applies to an arbitrary machine. For conciseness, “M ⊧” has been omitted from STAs in the hypothesis and conclusion of the laws.

1.8.1. The consequence rule

The following is similar to the rule of consequence of Hoare logic. It allows preconditions to be strengthened and postconditions to be weakened

A′ ⟹ A  P′ ⟹ P  A \overline{{Q \atop P}} \overline{>} B  B ⟹ B′  Q ⟹ Q′ ; A′  \overline{\begin{matrix}Q′ \\ P′ \end{matrix}} \overline{>} B′

1.8.2. The sequencing rule

The sequencing rule allows sequences of transitions to be combined into a single long transition.

A \overline{\begin{matrix}By δ_{1} ∧ [q_{1}] \\ [p_{1}] \end{matrix}}\overline{>} B B \overline{\begin{matrix}By δ_{2} ∧ [q_{2}] \\ [p_{2}] \end{matrix}}\overline{>} C ; A \overline{\begin{matrix}By(δ_{1}+δ_{2}) ∧ [q_{1} ∨ q_{2}] \\ [p_{1} ∧ p_{2}] \end{matrix}}\overline{>} C

This rule requires that the input preconditions [p_{1}] and [p_{2}] are conjoined in the conclusion, so that both p_{1} and p_{2} are required to hold throughout the combined transition. This is sufficient for the Mult example, but a stronger rule would have [p_{1}];[p_{2}] as the input precondition of the conclusion, where ; is a chop operator of interval temporal logic [3].

1.8.3. Cases rules There are two cases rules. One for case analysis of state preconditions:

A_{1}  \overline{{Q \atop P}} \overline{>} B  A_{2}  \overline{{Q \atop P}} \overline{>} B ; A_{1} ∨ A_{2} \overline{{Q \atop P}} \overline{>} B

and the other for case analysis of input preconditions:

A \overline{{Q \atop P_{1}}} \overline{>} B A \overline{{Q \atop P_{2}}} \overline{>} B ; A \overline{\begin{matrix}Q \\ P_{1} ∨ P_{2} \end{matrix}}\overline{>} B

A combination of sequencing and cases can be used to establish the resetting behaviour:

              MultMachine ⊧ True \overline{\begin{matrix}By 43 \\ [reset ≡ 1] \end{matrix}}\overline{>} At(MultProg) 0

The argument proceeds by first splitting the universally true predicate True into a 20-way disjunction asserting that control is either outside the program or is inside one of the intermediate commands. For each case, the sequencing rule applied to atomic STAs can be used to show that under the assumption of reset ≡ 1 the postcondition At(MultProg) 0 is eventually achieved. Showing these amounts to symbolic execution from an arbitrary starting position. The results of each of these cases are combined using a cases rule. Although there is a substantial amount of detail, a reset-analysis tool has been implemented that performs the proof automatically.

1.8.4. The wait loop rule

The next STA rule enables the existence of wait states to be deduced. Unfortunately the rule is rather complicated and contains a number of hypotheses that are hard to motivate in a general way (their necessity only becomes apparent when the detailed derivation of the rule is considered, which is not done here).

To see why waiting states can be rather subtle consider MultSpec. To meet this specification it is necessary to have a predicate, Ready z say, that satisfies both

Ready z ⟹ (avail ≡ 1 ∧ out ≡ z)

and req ≡ 0 Holds (Ready z)

Consider now the execution of MultProg when it is waiting to start a handshake. It will be cycling between intermediate commands 0, 1 and 18 waiting for req to become 1 (see Figure 1.1). Abbreviate In(MultProg) to In. Perhaps Ready z could be defined by:

Ready z =_{def ?} (In 0 ∨ In 1 ∨ In 18) ∧ (avail ≡ 1 ∧ out ≡ z)

Unfortunately this definition will not ensure req ≡ 0 Holds (Ready z). To see this suppose control is at machine instruction 3 (JMZ 44), avail is 1 and out is z. The predicate In 1 will be true (since machine instruction 3 is part of intermediate command 1) and hence Ready z is true. Suppose now that the environment makes input req be 0. If req ≡ 0 Holds (Ready z) then the next state of the machine (i.e. the one after executing JMZ 44) must satisfy Ready z, however this will only be the case if the top of the stack contains 0, which will only be the case if req were true on the previous cycle (i.e. when INP req was executed). Thus req being 0 at instruction 3 does not ensure that Ready z is held. It is necessary to assume that the top of the stack is 0 rather than that the input req is 0. Thus the definition of Ready given above will not work. The solution used by the wait loop rule is to define Ready z to be true of a state σ if σ is reachable from a state satisfying At 1 via a trace in which all the intermediate states satisfy the invariant avail ≡ 1 ∧ out ≡ z and all the intermediate inputs satisfy req ≡ 0. If this is the case then machine instruction 3 will have been reached from a preceding state in which 0 was read onto the top of the stack.

In the complicated looking rule that follows, the predicate A characterizes the top of a wait loop. If the environment maintains the holding condition p_{1}, then the waiting is maintained and A is true each time the loop starts a new iteration. The invariant q holds during the wait loop. The predicate B is true of the first state not in the loop; it is reached if the environment maintains the breakout condition p_{2} for at least δ_{1} machine cycles. The first and last hypotheses of the rule are necessary technical conditions. The first hypothesis says that the breakout state is not passed though during the wait loop. The last hypothesis says that if the loop is started then no matter what inputs arrive, within δ_{2} cycles control will either return to the top of the loop or have left the loop.

\frac{(q ⟹ ¬B) ∧ (A \overline{{[q] \atop [p_{1}]}} \overline{>} A) ∧ (A \overline{\begin{matrix}By δ_{1} \\ [p_{2}] \end{matrix}} \overline{>} B) ∧ (A \overline{\begin{matrix}By δ_{2} \\ True \end{matrix}}\overline{>} A ∨ B)}{∃ W . (p_{1} Holds W ) ∧ (W \overline{\begin{matrix}By(δ_{1}+δ_{2}) \\ [p_{2}] \end{matrix}}\overline{>} B) ∧ (A ⟹ W ) ∧ (W ⟹ q)}

The application of this rule to MultProg is now shown. The hypotheses of the application are the following four facts. The first one follows directly from definitions; the other three can be deduced from automatically generated atomic STAs.

(In 0 ∨ In 1 ∨ In 18) ∧ ( avail ≡ 1 ∧ out ≡ z) ⟹ ¬(At 2 ∧ avail ≡ 1 ∧ out ≡ z)

 At 1 ; avail ≡ 1 ; out ≡ z

[ \begin{matrix}In 0 ∨ In 1 ∨ In 18 \\ avail ≡ 1 ∧ out ≡ z \end{matrix} ]
[req ≡ 0]

>

                                   At 1 ; avail ≡ 1 ; out ≡ z

 At 1 ; avail ≡ 1 ; out ≡ z \overline{\begin{matrix}By 2 \\ [req ≡ 1] \end{matrix}}\overline{>} At 2 ; avail ≡ 1 ; out ≡ z

At 1 ; avail ≡ 1 ; out ≡ z \overline{{By 5 \atop True}}\overline{>} ( \begin{matrix}At 1 \\ avail ≡ 1 \\ out ≡ z \end{matrix} ∨ \begin{matrix}At 2 \\ avail ≡ 1 \\ out ≡ z \end{matrix} )

From these hypotheses, the wait loop rule directly yields the existence of a predicate W z such that:

(req ≡ 0) Holds (W z)

and

W z \overline{\begin{matrix}By 7 \\ [req ≡ 1] \end{matrix}}\overline{>} At 2 ; avail ≡ 1 ; out ≡ z

and

At 1 ∧ avail ≡ 1 ∧ out ≡ z ⟹ W z

and

W z ⟹ (In 0 ∨ In 1 ∨ In 18) ∧ ( avail ≡ 1 ∧ out ≡ z)

The desired result is obtained by defining Ready to be W . The application of the wait loop rule has been fully automated and so most of the details just shown are generated by a procedure and need not concern the user. The existence of a predicate Ack x y z can be deduced similarly.

1.8.5. The while rule

The while rule for STAs is analogous to the while rule of a Hoare logic of total correctness. It is formulated here in terms of predicates on stack machine states, though it could be expressed abstractly in terms of arbitrary predicates as was done for the wait loop rule. First some notation. A vector of names ⟨x_{1}, …, x_{n}⟩ will be abbreviated to x⃗ and similarly a vector ⟨x_{1}, …, x_{n}⟩ of values will be abbreviated to x⃗. The predicate x⃗ ≡ x⃗ abbreviates the conjunction of predicates x_{1} ≡ x_{1} ∧ … ∧ x_{n} ≡ x_{n}. The predicate v ≪ x is true of a state (pc, stk, mem) iff mem v < x. If f is a function from vectors of values to vectors of values and A, B are predicates on vectors of values, then the Hoare logic like notation {A}f {B} means ∀ x⃗. A x⃗ ⇒ B(f x⃗).

In the while rule for STAs that follows, Inv and B are arbitrary predicates on vectors of values called the invariant and test, respectively. The function f specified the statechange each time around the loop (i.e. the ‘meaning’ of the body of the ‘while loop’). The first hypothesis of the rule says that Inv is an invariant and the value of x_{i} decreases each time around the loop (i.e. x_{i} is a variant). The second hypothesis is that the loop starts with the values x⃗ of x⃗ in the memory satisfying Inv. It is assumed that the top of a while loop is at itermediate command n. If the test B fails, the loop exits to the command numbered n_{2}, without change of memory and taking δ_{1} cycles. If B succeeds then control transfers to n_{1}, without changing the memory and taking δ_{1} cycles, and then back to n with the memory changed by f and taking another δ_{2} cycles.

Thus while B remains true the program loops from n to n_{1} then back to n taking δ_{1} + δ_{2} cycles and transforming the values of the vector of variables x⃗ by f each time. The conclusion of the rule is that the loop will terminate within δ_{1} +(δ_{1}+δ_{2})×x_{i} cycles, where x_{i} is the value of the variant x_{i} when the loop started. On termination the invariant still holds, but the test B is false. Here is the while rule for STAs.

{Inv ∧ B ∧ x_{i} ≡ x_{i}} f {Inv ∧ x_{i} ≪ x_{i}}

Inv x⃗

∀ x⃗. ( \begin{matrix}At n \\ x⃗ ≡ x⃗ \end{matrix} \overline{\begin{matrix}By δ_{1} \\ [p_{1}] \end{matrix}}\overline{>} At(B x⃗ → n_{1} | n_{2}) x⃗ ≡ x⃗ )

∀ x⃗. ( \begin{matrix}At n_{1} \\ x⃗ ≡ x⃗ \end{matrix} \overline{\begin{matrix}By δ_{2} \\ [p_{2}] \end{matrix}}\overline{>} \begin{matrix}At n \\ x⃗ ≡ f x⃗ \end{matrix} )

∃ x′. ( \begin{matrix}At n \\ x⃗ ≡ x⃗ \end{matrix} \overline{\begin{matrix}By(δ_{1} + (δ_{1}+δ_{2}) × x_{i}) \\ [p_{1} ∧ p_{2}] \end{matrix}}\overline{>} \begin{matrix}At n_{2} \\ x⃗ ≡ x′ \end{matrix} ) ∧ Inv x′ ∧ ¬(B x′)

As an example of the STA while rule consider the iteration:

 WHILE (x > O) AND NOT(INPUT reset)
  DO out := out + y;
     x   := x - 1
  OD

This translates to the following intermediate form (see Figure 1.1).

 13: IF x > 0 AND NOT(INPUT reset) THEN SKIP ELSE GOTO 17 .. 27: GET x
                                                             28: OP0 0
                                                             29: OP2 >
                                                             30: INP reset
                                                             31: OP1 NOT
                                                             32: OP2 AND
                                                             33: JMZ 42
 14: out := out + y ........................................ 34: GET out
                                                             35: GET y
                                                             36: OP2 +
                                                             37: PUT out
 15: x := x - 1 ............................................ 38: GET x
                                                             39: OP1 pre
                                                             40: PUT x
 16: GOTO 13 ............................................... 41: JMP27

From which the following two STAs can be generated (the free variables reset, x, y and out are assumed to be universally quantified).

At 13 ; x ≡ x ; y ≡ y ; out ≡ out By 7

[reset ≡ reset]

>

At(x > 0 ∧ ¬(reset = 1) → 14 | 17)
x ≡ x
y ≡ y
out ≡ out

At 14 ; x ≡ x ; y ≡ y ; out ≡ out

{By 8 \atop True} >

                   At 13

x ≡ x − 1 y ≡ y out ≡ out + y For arbitary r take:

Inv_{r}⟨x, y, out⟩ = (out+(x×y) = r)
B⟨x, y, out⟩ = x > 0 ∧ ¬(reset = 1)
f ⟨x, y, out⟩  = ⟨x−1, y, out+y⟩

It follows that {Inv_{r} ∧ B ∧ x ≡ m} f {Inv_{r} ∧ x < m} and hence by the while rule, if out+(x×y) = r then there exists x′, y′ and out′ such that:

( At 13 ; x ≡ x ; y ≡ y ; out ≡ out \overline{By(7 + (7+8) × x) [reset ≡ reset]}\overline{>} At 17 ; x ≡ x′ ; y ≡ y′ ; out ≡ out′ ) ∧ Inv_{r}⟨x′, y′, out′⟩ ∧ ¬B⟨x′, y′, out′⟩

Hence out′+(x′×y′) = r (the invariant still holds) and ¬(x′ > 0 ∧ ¬(reset = 1)) (the test is false). If reset = 0 then it follows from the test being false that x′ = 0 and then if r is taken to be x × y it follows from the invariant still holding that out′ = x × y. Hence:

At 13 ; x ≡ x ; y ≡ y ; out ≡ 0

By(7+15×x) [reset ≡ 0]

>

At 17 ; x ≡ 0 ; y ≡ y′ ; out ≡ x×y

By choosing a slightly more complex invariant it could also be shown that the value of y is unchanged by the iteration.

1.9. Conclusions

The analysis of real-time programs is notoriously complex. The approach outlined here tightly couples the formalism used (STAs) with theorem proving tools, the aim being to automate away as much detail as possible. The current mechanization requires the user to invoke tools, such as the wait loop synthesizer and the while rule, on an intermediate representation of the high-level program consisting of sequences of assignments and jumps. In the future, it is hoped to try to hide this level completely by guiding the verification via annotations in the program. The goal, only partially achieved so far, is to require the user to manually prove ‘mathematical’ verification conditions, but to have all STA manipulations performed automatically. Progress towards this goal appears in the paper entitled ‘A Hoare logic of state transitions’ included in the Festschrift for Professor Hoare, edited by Bill Roscoe and published by Prentice-Hall in 1994. In that paper it is shown how the while rule for STAs can be automatically invoked via annotations in the high-level program. This is achieved by defining a Hoare logic of state transitions.

The approach taken here can be viewed as lying somewhere in the middle of a spectrum with conventional verification plus a verified compiler at one end, and pure machine code verification at the other. Conventional verification using a high-level semantics has many advantages: properties of programs can be proved that are independent of the compiler used. If a verified compiler is available, then analysis can be conducted within an abstract semantics and then applied, via a compiler correctness statement, to machine code [2].

At the other extreme, one can model the host machine semantics and then verify machine code programs (got, for example, by running production Ada compilers) by reasoning about processor transitions. Impressive work of this sort has been done by Yuan and Boyer [6]. Between these two extremes lies the work presented here. The techniques are in the spirit of Yuan and Boyer in that they are based on a semantics derived from the execution of machine instructions (though Yuan and Boyer use a real machine in the 68000 family, whereas an enormously simpler abstract machine is used here). However, the reasoning is conducted through an abstract view of the machine code provided by a high level programming language. Proofs are conducted using Hoare-style proof rules normally associated with high-level languages; but the interpretation of the Hoare-sentences is lowlevel.

24 CHAPTER 1. STATE TRANSITION ASSERTIONS: A CASE STUDY

Bibliography

REFERENCES

1 J. A. Camilleri. Symbolic compilation and execution of programs by proof: A case study in HOL. Technical Report 240, Computer Laboratory, University of Cambridge, UK, December 1991.

2 P. Curzon. Deriving correctness properties of compiled code. In L. Claesen and M. Gordon, editors, Proceedings of the International Workshop on Higher Order Logic Theorem Proving and its Applications. North-Holland, 1992.

3 J. Halpern, Z. Manna, and B. Moszkowski. A hardware semantics based on temporal intervals. In Proc. 10th International Colloquium on Automata, Languages and Programming, Barcelona, Spain, 1983.

4 C. A. R. Hoare. An axiomatic basis for computer programming. Communications of

the ACM, 12:576–583, October 1969. 5 B. Levy, I. Filippenko, L. Marcus, and T. Menas. Using the state delta verification

system. In Proc. IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design, pages 337–360. North-Holland, June 1992.

6 Y. Yu. Automated Proofs of Object Code for a Widely Used Microprocessor. PhD thesis, The University of Texas at Austin, yuanyu@com.dec.src, 1992.