mbind operator
CodeArtifactThe mbind operator is used in HOL-TestGen sequence-test specifications over the state-exception monad. It iterates an input/output stepping function over a list of inputs, feeding each input to the system under test and stopping when an error occurs.
First seen 5/26/2026
Last seen 5/26/2026
Evidence 3 chunks
Wiki v1
WIKI
Overview
mbind is an operator used for sequence-test specifications in HOL-TestGen. It is introduced for iterations of input/output stepping functions: given a list of inputs ιs = [i1, ..., in], it feeds the inputs subsequently into the system under test (SUT) and stops when an error occurs. This gives a compact representation of valid test sequences for programs under test.
σ |= os ← mbind ιs SUT; return (P os)
NEIGHBORHOOD
No graph connections found for this entity yet. It may appear in future ingestion runs.
explore full graph →RELATIONSHIPS
2 connectionsThe paper uses the mbind operator in test sequence specifications.
mbind uses the state-exception monad to iterate over a list of inputs.
CITATIONS
9 sources9 citations — click to expand
[1] mbind iterates a list of inputs through an input/output stepping function, feeds the inputs subsequently into the SUT, and stops when an error occurs. Test Program Generation for a Microprocessor: A Case Study
[2] HOL-TestGen uses monads for sequence test specifications because HOL has no built-in concepts for states and state transitions. Test Program Generation for a Microprocessor: A Case Study
[3] The state-exception monad models partial state-transition functions of type (o, σ) MONSE = σ ⇀ (o × σ), and programs under test can be seen as stepping functions of type ι ⇒ (o, σ) MONSE. Test Program Generation for a Microprocessor: A Case Study
[4] Using mbind with return is described as HOL-TestGen's standard way to represent sequence test specifications. Test Program Generation for a Microprocessor: A Case Study
[5] For state-dependent post-conditions, the source uses assertSE instead of return and defines assertSE as a state-exception primitive. Test Program Generation for a Microprocessor: A Case Study
[6] execVAMP is defined as a lifting of exec_instr into the state-exception monad. Test Program Generation for a Microprocessor: A Case Study
[7] The source gives a load/store mbind example using Isw and Ilbu instructions and maps it to an ISW/LLBU assembly sequence. Test Program Generation for a Microprocessor: A Case Study
[8] The source gives an arithmetic mbind sequence example using Isub and Iadd instructions. Test Program Generation for a Microprocessor: A Case Study
[9] The case study states that sequence test programs can reveal read/write sequencing errors such as byte-alignment errors or information loss due to pipelining. Test Program Generation for a Microprocessor: A Case Study