Documentation

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)