Overview

bindSE is the monadic bind operator defined for the state-exception monad used in HOL-TestGen. In the cited microprocessor test-generation case study, this monad is used because HOL is a purely functional specification formalism and has no built-in notions of state or state transitions. The state-exception monad models partial state-transition functions of the form:

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

A computation in this monad may fail for a given state, represented by None, or return an output together with a successor state, represented by Some(out, σ').

Definition

The paper defines bindSE as follows:

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

Operationally, bindSE f g first applies computation f to the current state σ. If f σ is None, the composed computation also fails. If f σ returns Some(out, σ'), then bindSE continues by applying g to the output out and successor state σ'.

Role in sequence specifications

The source describes bind as representing sequential composition with value passing. For the state-exception monad, bindSE provides that behavior for computations that both observe outputs and update state. The associated unitSE operator embeds a value into a computation:

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

The notation:

x ← f; g

is used for:

bindSE f (λx. g)

and return is used for unitSE.

Use in HOL-TestGen

In HOL-TestGen sequence-test specifications, programs under test can be modeled as input/output stepping functions of type:

ι ⇒ (o, σ) MONSE

Each stepping function either fails for a given state and input, or produces an output and successor state. Using bindSE, a valid test sequence can be expressed as a sequence of system-under-test invocations followed by a returned postcondition result, for example:

σ |= o₁ ← SUT i₁; ...; on ← SUT iₙ; return (P o₁ ... oₙ)

For repeated application over a list of inputs, the paper also describes an mbind operator that feeds inputs into the system under test and stops when an error occurs. In cases where a postcondition depends explicitly on the underlying state, the paper uses the assertSE primitive instead of return(P).