Overview

The state-exception monad is a modeling device used by HOL-TestGen for sequence test specifications in a purely functional HOL setting, where states and state transitions are not built in. It is described as well fitted for modeling partial state-transition functions of the form:

type_synonym (o, σ) MONSE = σ ⇀ (o × σ)

In this representation, a computation maps a state σ either to failure or to a pair consisting of an output o and a successor state. [State-transition model]

Role in sequence testing

For programs under test, the monadic view represents an input/output stepping function as:

ι ⇒ (o, σ) MONSE

Such a stepping function may fail for a given state and input, or it may produce an output and a successor state. This supports sequence-oriented tests, where tests describe sequences of state transitions performed while executing program instructions. [I/O stepping functions]

HOL-TestGen uses this monadic formulation because HOL is a purely functional specification formalism without built-in concepts for mutable states and transitions. [HOL-TestGen use]

Core operations

The usual monadic operations are defined for the state-exception monad:

definition bindSE :: (o, σ) MONSE ⇒ (o ⇒ (o’, σ) MONSE) ⇒ (o’, σ) MONSE
where bindSE f g = λσ. case f σ of None ⇒ None
        | Some(out, σ’) ⇒ g out σ’

 definition unitSE :: o ⇒ (o, σ) MONSE
where unitSE e = λσ. Some(e, σ)

Here, bindSE represents sequential composition with value passing, while unitSE embeds a value into a computation. The notation x ← f; g abbreviates bindSE f (λx. g), and return abbreviates unitSE. [Bind and unit]

Sequence specifications with mbind

For iterations of input/output stepping functions, the mbind operator takes a list of inputs and feeds them sequentially into the system under test, stopping when an error occurs. HOL-TestGen represents sequence test specifications in the form:

σ |= os ← mbind ιs SUT; return(P os)

where ιs = [i1, ..., in] is the input sequence and P is a post-condition over the observed outputs. [mbind sequence form]

State-dependent post-conditions

When a post-condition depends explicitly on the underlying state, the state-exception primitive assertSE is used instead of return(P):

definition assertSE :: (σ ⇒ bool) ⇒ (o, σ) MONSE
where assertSE P = (λσ. if P σ then Some(True, σ) else None)

This allows a test specification to assert predicates over the final state reached by a sequence. [assertSE]

VAMP case-study use

In the VAMP microprocessor test-generation case study, sequence test scenarios include tests over the final processor state. The case study gives examples comparing either the entire final state or a selected part of it, such as register 0, after executing a generated instruction sequence. [Final-state testing]

The function execVAMP is defined as a lifting of exec_instr into the state-exception monad:

definition execVAMP where execVAMP ≡ (λ i σ. Some ((), exec_instr σ i))

In the same setting, σ0 denotes the initial state and ιs denotes the sequence of generated instructions. [execVAMP lifting]

Test purposes

The case study also notes that preconditions, called test purposes, are added to test specifications to reduce generated instruction sequences to a selected subset. For example, a load/store test purpose can restrict a scenario to load and store instructions. [Test purposes]