Module Monolith

The submodule Gen offers facilities for generating values of many common types.

A value of type 'a gen is a generator of values of type 'a.

We use the PPrint library to pretty-print OCaml code.

The submodule Print offers facilities for printing OCaml values and expressions.

A value of type 'a gen is a printer of values of type 'a.

A value of type appearance is a printable representation an OCaml expression. One can think of the type appearance almost as synonym for the type document. In particular, the function document is an injection of document into appearance. The type appearance offers a few bells and whistles that the type document does not have; these include the ability to print applications in a customized manner.

constant is an injection of string into appearance. The appearance constant c is printed as the string c (without quotes).

document is an injection of document into appearance. The appearance document doc is printed as the document doc.

infix op is an appearance for an OCaml infix operator named op, where op is the name of the operator, without parentheses. This appearance is set up so that an application of it to exactly two actual arguments is printed infix. An application of it to more or fewer than two actual arguments is printed using normal application syntax.

A value of type 'a code is a pair of a value of type 'a and a printable representation of this value. Several specification combinators, including constructible, deconstructible, declare_abstract_type, map_into, and map_outof expect an argument of type 'a code.

A specification of type ('r, 'c) spec describes a value whose type on the reference side is 'r and whose type on the candidate side is 'c.

constructible generate describes a basic constructible type, that is, a type 't that is equipped with a generator.

The function generate must have type unit -> 't code, which means that it must produce a pair of a value and a printable representation of this value. (See also the combinator constructible_, which has slightly different requirements.)

It is worth noting that constructible can be used, if desired, to construct a value whose type is a function type.

When a value must be constructed, the function generate is applied once, and the value thus obtained is used both on the reference side and on the candidate side. This explains why the return type of this combinator is ('t, 't) spec.

This specification is constructible.

easily_constructible generate print describes a basic constructible type, that is, a type 't that is equipped with a generator.

It is a special case of constructible. It is less powerful, but is easier to use.

The function generate must have type 't gen. The function print must have type 't printer. These functions are combined to obtain a generator of type unit -> 't code, which is used in a call to constructible.

This specification is constructible.

deconstructible ~equal print describes a basic deconstructible type, that is, a type 't that is equipped with an equality test and with a printer.

The equality test equal is used to compare the values produced by the reference implementation and by the candidate implementation. (The reference value is the first argument; the candidate value is the second argument.)

The argument equal is optional. If it is omitted, then OCaml's generic equality function (=) is used.

Because the reference value and the candidate value are expected to have the same type, the return type of this combinator is ('t, 't) spec.

This specification is deconstructible.

declare_abstract_type() declares a new abstract type, whose values on the reference side have type 'r and whose values on the candidate side have type 'c.

An abstract type is usually implemented in different ways in the reference implementation and in the candidate implementation. For instance, a sequence may be represented as a linked list in the reference implementation and as a resizeable array in the candidate implementation.

The optional parameter check is a well-formedness check. If present, this function is applied by Monolith, after every operation, to every data structure of this abstract type that is currently at hand. This allows checking after every operation that every data structure remains well-formed.

The check function is applied to two arguments, namely, the reference data structure of type 'r and the candidate data structure of type 'c.

If all is well, then check should return (). If something is wrong, then check should raise an exception, such as Assertion_failure _.

It is up to the user to decide how thorough (and how costly) the well-formedness check should be. Checking that the candidate data structure seems well-formed, while ignoring the reference data structure, is a possibility. Checking that the candidate data structure is well-formed and is in agreement with the reference data structure is the most comprehensive check that can be performed.

The optional parameter var is a base name that is used for variables of this abstract type.

This specification is constructible and deconstructible.

Because declare_abstract_type declares an abstract type as a side effect, it cannot be used under a dependent arrow ^>>. It is recommended to use it at the top level only.

unit represents the base type unit.

This specification is constructible and deconstructible.

bool represents the base type bool.

This specification is constructible and deconstructible.

int represents the basic deconstructible type int.

This specification is deconstructible. It is not constructible, because it usually does not make sense to generate an integer in the huge interval [min_int, max_int].

int_within range is the basic type int, equipped with the generator range.

This specification is constructible and deconstructible.

semi_open_interval i j is int_within (Gen.semi_open_interval i j).

closed_interval i j is int_within (Gen.closed_interval i j).

lt j is int_within (Gen.lt j).

le j is int_within (Gen.le j).

sequential() is int_within (Gen.sequential()).

exn represents the base type exn.

This specification is deconstructible, but not constructible.

override_exn_eq f overrides the notion of equality that is associated with the type exn. This notion of equality is used to compare an exception raised by the reference implementation with an exception raised by the candidate implementation. By default, it is OCaml's generic equality (=), which means that both implementations must raise exactly the same exceptions. override_exn_eq allows relaxing this requirement. The function f receives the current notion of equality as an argument and is expected to return a new notion of equality, which is installed in place of the previous one.

ignored describes a result that should be ignored.

This specification is deconstructible, but not constructible.

*** is the pair type constructor.

When applied to constructible specifications, it produces a constructible specification. When applied to deconstructible specifications, it produces a deconstructible specification.

option is the option type constructor.

When applied to a constructible specification, it produces a constructible specification. When applied to a deconstructible specification, it produces a deconstructible specification.

result is the result type constructor.

When applied to constructible specifications, it produces a constructible specification. When applied to deconstructible specifications, it produces a deconstructible specification.

list ~length is the list type constructor.

When applied to a constructible specification, it produces a constructible specification. When applied to a deconstructible specification, it produces a deconstructible specification.

When this specification is used in construction mode, the generator length controls the length of the lists that are generated. The length parameter is optional; if is omitted, Gen.lt 16 is used. When this specification is used in deconstruction mode, the length parameter is irrelevant.

Using the combinator nondet allows the reference implementation to have access to the candidate result of type 'c produced by the candidate implementation. It must then produce a diagnostic of type 'r diagnostic.

The diagnostic Valid r means that the candidate result is acceptable and that the corresponding reference result is r.

The diagnostic Invalid cause means that the candidate result is wrong. The function cause is an explanation why the candidate result is unacceptable. This function is applied to the name of a variable, such as observed, which stands for the candidate result. It is expected to produce a piece of OCaml code that pinpoints the problem. This code could be an OCaml assertion that the observed result does not satisfy, such as assert (observed > 0). It could also be just a comment, such as (* candidate finds -2, whereas a positive number was expected *). Or, it could be a combination of both. The module Print can help construct such OCaml code.

In the common case where 'r and 'c are the same type, the following type abbreviation is useful. Then, using the combinator nondet changes the type of the reference implementation from 'r to 'r nondet.

nondet spec describes the result of an operation whose specification is nondeterministic. It indicates that several results are permitted. Therefore, one cannot expect the reference implementation to produce "the" expected result. Instead, Monolith must run the candidate implementation first, and allow the reference implementation to have access to the result c produced by the candidate. The reference implementation is then expected to return a result of type 'r diagnostic. If the reference implementation returns Valid r, then the deconstruction process continues: that is, the reference result r and the candidate result c are deconstructed in the manner specified by spec.

When 'r and 'c are in fact the same type, the type of nondet can be written under the form ('t, 't) spec -> ('t nondet, 't) spec.

nondet must be applied to a deconstructible specification, and produces a deconstructible specification.

^> is the ordinary arrow combinator. It describes a function of one argument. By using it several times, one can also describe curried functions of several arguments, which are common in OCaml. This combinator imposes the absence of exceptions: the reference and candidate implementations are expected to not raise any exception.

In an application domain ^> codomain, the specification domain must be constructible, while codomain must be either a function specification or deconstructible. The specification domain ^> codomain is neither constructible nor deconstructible.

^?> is the nondeterministic arrow combinator. spec1 ^?> spec2 is a short-hand for spec1 ^> nondet spec2.

The (de)constructibility constraints are the same as with an ordinary arrow (^>).

^!> is the exceptional arrow combinator. It describes a function that may raise an exception, and it requests that this exception be caught and observed. This implies that the reference and candidate implementations are expected to raise an exception under the same circumstances, and are expected to raise comparable exceptions, according to the notion of equality that exists at type exn. This notion of equality can be customized by using override_exn_eq.

The (de)constructibility constraints are the same as with an ordinary arrow (^>).

^!?> is an arrow combinator that combines the exception effect and the nondeterminism effect. It describes a function that may raise an exception. Furthermore, it allows nondeterminism: the candidate implementation is allowed to decide whether it wishes to return normally or to raise an exception; it is also allowed to decide what exception it wishes to raise. To deal with this flexibility, the behavior of the candidate implementation is reified as a value of type ('c2, exn) result, which the reference implementation receives as an argument. The reference implementation is then expected to either accept or reject this candidate behavior, which it does by returning a diagnostic. If it decides to accept this behavior, then it must return its own behavior as a value of type ('r2, exn) result. The reference implementation must never raise an exception.

The (de)constructibility constraints are the same as with an ordinary arrow (^>).

^>> is the dependent arrow constructor. It describes a function of one argument and allows naming (the reference side of) this argument, so that this argument can be referred to in the codomain.

For example, the specification of a get function in a sequence might be seq ^>> fun s -> lt (length s) ^> element. The first argument, a sequence, receives the name s. This allows specifying that the second argument, an integer, must lie in the semi-open interval [0, length s). Here, the variable s denotes the data structure built by the reference implementation, so length must be the reference-side function that maps a sequence to its length.

The (de)constructibility constraints are the same as with an ordinary arrow (^>).

% is the subset constructor. It restricts the set of arguments that can be passed to an operation; in other words, it expresses a precondition. For example, to express the fact that the operation pop must be applied to a nonempty stack, one can use nonempty % stack, where the reference-side function nonempty tests whether a stack is nonempty, and stack is the abstract type of stacks.

% must be applied to a constructible specification, and produces a constructible specification.

map_outof specifies that a transformation must be applied to a value. The user must provide the reference side of the transformation, the candidate side of the transformation, and a specification of the input type of the transformation. It is typically used to transform an argument before passing it to an operation.

map_outof must be applied to a constructible specification, and produces a constructible specification.

map_into specifies that a transformation must be applied to a value. The user must provide the reference side of the transformation, the candidate side of the transformation, and a specification of the output type of the transformation. It is typically used to transform the result of an operation, or an operation itself.

map_into must be applied to a deconstructible specification, and produces a deconstructible specification.

flip exchanges the first two arguments of a curried function.

rot2 moves the second argument of a curried function to the first position. It is synonymous with flip.

rot3 moves the third argument of a curried function to the first position. It is synonymous with flip.

curry transforms a function that expects a pair into a function that expects two separate arguments.

uncurry transforms a function that expects two separate arguments into a function that expects a pair.

The conditional specification ifpol neg pos is interpreted as the specification neg when it is used in construction mode (that is, when it describes the input of an operation) and as the specification pos when it is used in deconstruction mode (that is, when it describes the output of an operation).

ifpol is a low-level combinator that is typically used to define higher-level abstractions.

In an application ifpol neg pos, the specification neg must be constructible, the specification pos must be deconstructible, and the result is both constructible and deconstructible.

fix builds a recursive specification.

The function call declare_semi_abstract_type spec declares a new abstract type t and equips it with one operation, namely a one-way conversion from t to spec, whose implementation is the identity function.

This is typically used to disguise a function type as an abstract type. For instance, if an operation has type a -> b -> c and if one wishes Monolith to perform a partial application, then one should declare b ^> c as a semi-abstract type t and use the specification a ^> t.

declare_semi_abstract_type must be applied to a deconstructible specification, and produces a deconstructible specification.

Because declare_semi_abstract_type declares an abstract type as a side effect, it cannot be used under a dependent arrow ^>>. It is recommended to use it at the top level only.

declare_seq ~length is a persistent sequence type constructor.

When applied to a constructible specification, it produces a constructible specification. When applied to a deconstructible specification, it produces a deconstructible specification.

When this specification is used in construction mode, the generator length controls the length of the sequences that are generated. The length parameter is optional; if is omitted, Gen.lt 16 is used. When this specification is used in deconstruction mode, the length parameter is irrelevant.

When this specification is used in deconstruction mode, it is treated as an abstract type, equipped with an operation that demands the first element of the sequence. It is possible for a sequence to be demanded several times.

A sequence is not allowed to raise an exception when it is demanded: such an event is considered an error.

Because declare_seq declares an abstract type as a side effect, it cannot be used under a dependent arrow ^>>. It is recommended to use it at the top level only.

declare_affine_seq ~length is an affine sequence type constructor.

When applied to a constructible specification, it produces a constructible specification. When applied to a deconstructible specification, it produces a deconstructible specification.

When this specification is used in construction mode, the generator length controls the length of the sequences that are generated. The length parameter is optional; if is omitted, Gen.lt 16 is used. When this specification is used in deconstruction mode, the length parameter is irrelevant.

When this specification is used in deconstruction mode, it is treated as an abstract type, equipped with an operation that demands the first element of the sequence. An affine sequence is demanded at most once.

A sequence is not allowed to raise an exception when it is demanded: such an event is considered an error.

Because declare_affine_seq declares an abstract type as a side effect, it cannot be used under a dependent arrow ^>>. It is recommended to use it at the top level only.

declare name spec reference candidate declares the existence of an operation. Its parameters are the name of this operation, its specification, and its implementations on the reference side and on the candidate side.

declare can be called either before main is invoked or from the function prologue that is passed as an argument to main. It cannot be used under a dependent arrow ^>>.

main fuel sets up and starts the engine.

main parses the command line and sets up the engine to draw data from the file whose name is supplied on the command line. If no file name is supplied, data is drawn from /dev/urandom.

The parameter fuel is the maximum length of a run (expressed as a number of operations). A small value, such as 5, 10, or 20, is typically used.

An optional prologue can be supplied. If present, the function prologue is invoked once at the beginning of each run. It may invoke data generation functions in the module Gen, declare operations, and produce output using dprintf. Its purpose is to determine the global parameters of the run, if desired. For instance, if the library under test is a bounded stack and takes the form of a functor that expects a bound n, then the prologue can choose a value of n, apply the functor, and declare the operations thus obtained. The demo demos/working/stack_prologue illustrates this.

dprintf is analogous to printf. Its output is actually printed to the standard output channel only if a scenario that leads to a problem is discovered. In that case, it is printed at the beginning of the scenario.

This can be exploited, for instance, to print a number of global settings that have been made in the prologue.

dprintf can be called either before main is invoked or from the function prologue that is passed as an argument to main. It cannot be used under a dependent arrow ^>>.

The exception PleaseBackOff can be raised by the reference implementation of an operation to indicate that this operation (or this particular choice of arguments for this operation) should not be exercised. The reason could be that it is not permitted, or that it has not yet been implemented. This exception causes Monolith to silently back off and try another operation.

The reference implementation must not perform any side effect before raising this exception.

The exception Unimplemented can be raised by the candidate implementation of an operation to indicate that this operation (or this particular choice of arguments for this operation) should not be exercised. This exception causes Monolith to silently abandon the current scenario and investigate other scenarios.