The anyOptionalOutput function represents a specification for writing arbitrary optional output. The output can be anything, as indicated by the use of the wildcard pattern in its definition:

anyOptionalOutput = writeOptionalOutput [wildcard]

Represents a branching structure in a specification.

• The first Specification argument is the "then-case".
• The second Specification argument is the "else-case".

Represents a loop structure in a specification, performing the body while the condition holds.

The while function takes a condition and a body specification, and constructs a loop structure where:

• The Term 'Transparent Bool argument is the condition to be evaluated at the beginning of each iteration. The loop continues as long as the condition is True.
• The Specification argument is the body of the loop, executed while the condition is True.

The function assumes that the body specification does not contain a top-level exit marker.

while c bdy = tillExit (branch c bdy exit)

Represents a loop structure in a specification, performing the body while the condition does not hold.

The whileNot function takes a condition and a body specification, and constructs a loop structure where:

• The Term 'Transparent Bool argument is the condition to be evaluated at the beginning of each iteration. The loop continues as long as the condition is False.
• The Specification argument is the body of the loop, executed while the condition is False.

The function assumes that the body specification does not contain a top-level exit marker.

whileNot c bdy = tillExit (branch c exit bdy)

Represents a loop structure in a specification, performing the body at least once and then further while the condition does not hold.

The repeatUntil function takes a body specification and a condition, and constructs a loop structure where:

• The Specification argument is the body of the loop, executed at least once and then further times while the condition is False.
• The Term 'Transparent Bool argument is the condition to be evaluated at the end of each iteration. The loop continues until the condition becomes True.

The function assumes that the body specification does not contain a top-level exit marker.

repeatUntil bdy c = tillExit (bdy <> branch c exit nop)

Represents a loop structure in a specification, performing the body at least once and then further while the condition holds.

The doWhile function takes a body specification and a condition, and constructs a loop structure where:

• The Specification argument is the body of the loop, executed at least once and then further times while the condition is True.
• The Term 'Transparent Bool argument is the condition to be evaluated at the end of each iteration. The loop continues until the condition becomes False.

The function assumes that the body specification does not contain a top-level exit marker.

doWhile bdy c = tillExit (bdy <> branch c nop exit)

The (\\) operator computes set difference. It returns a ValueSet containing all integers of the first set that are not present in the second set.

Check if a given ValueSet of integers is empty.

This function uses an external SMT solver to check the constraints defined by the ValueSet.

Mandatory decoration of some term's result

Conceptually we have

writeOutput [decoratedResultOf t]
= writeOutput [nonEmptyWildcard <> resultOf t <> wildcard, wildcard <> resultOf t <> nonEmptyWildcard]

but matching failure will produce a specialized message

Values embeddable into a finite set of integers

Laws:

asInteger . asOriginal = id

For types with Eq instances that induce non-trivial equivalence classes, at least the weaker

asOriginal (asInteger x) == x = True

should hold. However program coverage is weakened in such scenarios, as generated inputs will only ever contain values from the co-domain of asOriginal.

Defined as currentValue = valueBefore 0, providing access to the current value.

Defined as allValues = valuesBefore 0, providing access to all values.

If the variable-expression x is associated with the values [x_1,..,x_n], valueBefore i x provides access to x_(n-i).

If the variable-expression x is associated with the values [x_1,..,x_n], valuesBefore i x provides access to [x_1,..,x_(n-i)].

Interpret a specification as a program in Monad m.

Returns a list containing all possible ways of resolving optionality, e.g.

>>> length (interpret $ writeOptionalOutput [x,y])
3