bindSE operator

CodeArtifact

The bindSE operator is the bind operation for the state-exception monad used in HOL-TestGen sequence test specifications. It composes partial state-transition computations sequentially: if the first computation fails, the result is failure; otherwise its output and successor state are passed to the next computation.

First seen 5/26/2026

Last seen 5/26/2026

Evidence 1 chunks

Wiki v1

WIKI

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 × σ)

READ FULL ARTICLE →

NEIGHBORHOOD

No graph connections found for this entity yet. It may appear in future ingestion runs.

explore full graph →

RELATIONSHIPS

1 connections

state-exception monad implements → 100% 1e

bindSE implements the bind operation of the state-exception monad.

LINKED ENTITIES

3 links

state-exception monad implements_bind_for The evidence explicitly defines bindSE as the bind operation for the state-exception monad with type MONSE.

mbind operator related_sequence_combinator The evidence describes mbind as an operator for iterations of input/output stepping functions in the same sequence-specification setting.

assertSE primitive related_state_exception_primitive The evidence defines assertSE as a state-exception primitive used when a postcondition depends on the underlying state.

CITATIONS

7 sources

7 citations — click to expand

[1] HOL-TestGen uses monads to support sequence test specifications because HOL has no built-in concepts for states and state transitions. Test Program Generation for a Microprocessor: A Case Study

[2] The state-exception monad is modeled as partial state-transition functions of type (o, σ) MONSE = σ ⇀ (o × σ). Test Program Generation for a Microprocessor: A Case Study

[3] Programs under test can be viewed as input/output stepping functions of type ι ⇒ (o, σ) MONSE that either fail or produce an output and successor state. Test Program Generation for a Microprocessor: A Case Study

[4] bindSE is defined with type (o, σ) MONSE ⇒ (o ⇒ (o', σ) MONSE) ⇒ (o', σ) MONSE and propagates None or passes Some(out, σ') to the next computation. Test Program Generation for a Microprocessor: A Case Study

[5] bind represents sequential composition with value passing, while unit represents embedding a value into a computation. Test Program Generation for a Microprocessor: A Case Study

[6] The notation x ← f; g is written for bindSE f (λx. g), and return is used for unitSE. Test Program Generation for a Microprocessor: A Case Study

[7] mbind feeds a list of inputs into the system under test and stops when an error occurs, and assertSE is used when a postcondition depends on the underlying state. Test Program Generation for a Microprocessor: A Case Study