monolith 20210525 · OCaml Package

Monolith offers facilities for testing an OCaml library by comparing its implementation (known as the candidate implementation) against a reference implementation.

For general information on Monolith and its workflow, please consult README.md and the paper Strong Automated Testing of OCaml Libraries, which describes the use and the design of Monolith in somewhat greater depth than this documentation.

This documentation is split up into the following parts:

Facilities for Generating Data.
Facilities for Displaying Data and Code.
Combinators for constructing Specifications.
Functions for setting up and starting the Monolith Engine.
Miscellaneous runtime Support functions.

Generating Data

module Gen : sig ... end

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

type 'a gen = 'a Gen.gen

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

Displaying Data and Code

type document = PPrint.document

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

module Print : sig ... end

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

type 'a printer = 'a Print.printer

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

type appearance

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.

val constant : string -> appearance

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

val document : document -> appearance

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

val infix : string -> appearance

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.

type 'a code = 'a * appearance

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.

Specifications

A specification is a description of an OCaml value. This value might be an argument for an operation, the result of an operation, or an operation itself.

When a value is meant to be used as an argument, Monolith must be able to construct such a value. In that case, a constructible specification must be given. For instance, lt 10 *** lt 10, which means a pair of integers less than 10, is a constructible specification.

When a value is a result, Monolith must be able to deconstruct such a value. In that case, a deconstructible specification must be given. For instance, option (int *** int), which means an optional pair of two integers, is a deconstructible specification.

When a value is an operation (a function), Monolith must be able to construct one or more arguments for this operation, to apply this operation, and to deconstruct the result. Thus, the arguments of a function type must be constructible, while its result must be deconstructible.

For instance, the specification of the pop operation on a stack could be nonempty % stack ^> element, which means pop expects a nonempty stack and returns an element. Or it could be stack ^!> element, which means pop expects a stack and either returns an element or raises an exception.

Equipping every operation with a specification is required for Monolith to know how many arguments the operation expects, what properties these arguments should satisfy, what result is produced, and what to do with this result.

Some specifications are constructible, but not deconstructible. For example, the combinator constructible yields specifications that are constructible, but not deconstructible.

Some specifications are deconstructible, but not constructible. A typical example is int. More generally, the combinator deconstructible yields specifications that are deconstructible, but not constructible.

Some specifications are both constructible and deconstructible. For example, the combinator ifpol yields specifications that are both constructible and deconstructible.

Some specifications are neither constructible nor deconstructible. As a typical example, the specification of an operation, built by the combinator (^>), is neither constructible nor deconstructible. This implies that Monolith has no direct support for higher-order functions.

type (_, _) spec

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.

The following combinators offer a wide variety of means of constructing specifications.

val constructible : (unit -> 't code) -> ('t, 't) spec

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.

val easily_constructible : 't gen -> 't printer -> ('t, 't) spec

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.

val deconstructible : 
  ?equal:('t -> 't -> bool) code ->
  't printer ->
  ('t, 't) spec

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.

val declare_abstract_type : 
  ?check:('r -> ('c -> unit) code) ->
  ?var:string ->
  unit ->
  ('r, 'c) spec

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.

val unit : (unit, unit) spec

unit represents the base type unit.

This specification is constructible and deconstructible.

val bool : (bool, bool) spec

bool represents the base type bool.

This specification is constructible and deconstructible.

val int : (int, int) spec

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].

val int_within : int gen -> (int, int) spec

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

This specification is constructible and deconstructible.

val semi_open_interval : int -> int -> (int, int) spec

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

val closed_interval : int -> int -> (int, int) spec

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

val lt : int -> (int, int) spec

lt j is int_within (Gen.lt j).

val le : int -> (int, int) spec

le j is int_within (Gen.le j).

val sequential : unit -> (int, int) spec

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

val exn : (exn, exn) spec

exn represents the base type exn.

This specification is deconstructible, but not constructible.

val override_exn_eq : ((exn -> exn -> bool) -> exn -> exn -> bool) -> unit

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.

val ignored : ('r, 'c) spec

ignored describes a result that should be ignored.

This specification is deconstructible, but not constructible.

val (***) : ('r1, 'c1) spec -> ('r2, 'c2) spec -> ('r1 * 'r2, 'c1 * 'c2) spec

*** 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.

val option : ('r, 'c) spec -> ('r option, 'c option) spec

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.

val result : 
  ('r1, 'c1) spec ->
  ('r2, 'c2) spec ->
  (('r1, 'r2) result, ('c1, 'c2) result) spec

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.

val list : ?length:int gen -> ('r, 'c) spec -> ('r list, 'c list) spec

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.

type 'r diagnostic =

| Valid of 'r
| Invalid of document -> document

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.

type 'r nondet = 'r -> 'r diagnostic

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.

val nondet : ('r, 'c) spec -> ('c -> 'r diagnostic, 'c) spec

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.

val (^>) : ('r1, 'c1) spec -> ('r2, 'c2) spec -> ('r1 -> 'r2, 'c1 -> 'c2) spec

^> 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.

val (^?>) : 
  ('r1, 'c1) spec ->
  ('r2, 'c2) spec ->
  ('r1 -> 'c2 -> 'r2 diagnostic, 'c1 -> 'c2) spec

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

The (de)constructibility constraints are stricter than those imposed by an ordinary arrow (^>). The domain must be constructible and the codomain must be deconstructible. The codomain cannot be an arrow.

val (^!>) : ('r1, 'c1) spec -> ('r2, 'c2) spec -> ('r1 -> 'r2, 'c1 -> 'c2) spec

^!> 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.

val (^!?>) : 
  ('r1, 'c1) spec ->
  ('r2, 'c2) spec ->
  ('r1 -> ('c2, exn) result -> ('r2, exn) result diagnostic, 'c1 -> 'c2) spec

^!?> 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.

val (^>>) : 
  ('r1, 'c1) spec ->
  ('r1 -> ('r2, 'c2) spec) ->
  ('r1 -> 'r2, 'c1 -> 'c2) spec

^>> 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 (^>).

val (%) : ('r -> bool) -> ('r, 'c) spec -> ('r, 'c) spec

% 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.

val map_outof : 
  ('r1 -> 'r2) ->
  ('c1 -> 'c2) code ->
  ('r1, 'c1) spec ->
  ('r2, 'c2) spec

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.

val map_into : 
  ('r1 -> 'r2) ->
  ('c1 -> 'c2) code ->
  ('r2, 'c2) spec ->
  ('r1, 'c1) spec

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.

val flip : 
  ('r1 -> 'r2 -> 'r3, 'c1 -> 'c2 -> 'c3) spec ->
  ('r2 -> 'r1 -> 'r3, 'c2 -> 'c1 -> 'c3) spec

flip exchanges the first two arguments of a curried function.

val rot2 : 
  ('r1 -> 'r2 -> 'r3, 'c1 -> 'c2 -> 'c3) spec ->
  ('r2 -> 'r1 -> 'r3, 'c2 -> 'c1 -> 'c3) spec

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

val rot3 : 
  ('r3 -> 'r1 -> 'r2 -> 'r4, 'c3 -> 'c1 -> 'c2 -> 'c4) spec ->
  ('r1 -> 'r2 -> 'r3 -> 'r4, 'c1 -> 'c2 -> 'c3 -> 'c4) spec

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

val curry : 
  ('r1 -> 'r2 -> 'r3, 'c1 -> 'c2 -> 'c3) spec ->
  (('r1 * 'r2) -> 'r3, ('c1 * 'c2) -> 'c3) spec

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

val uncurry : 
  (('r1 * 'r2) -> 'r3, ('c1 * 'c2) -> 'c3) spec ->
  ('r1 -> 'r2 -> 'r3, 'c1 -> 'c2 -> 'c3) spec

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

val ifpol : ('r, 'c) spec -> ('r, 'c) spec -> ('r, 'c) spec

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.

val fix : (('r, 'c) spec -> ('r, 'c) spec) -> ('r, 'c) spec

fix builds a recursive specification.

val declare_semi_abstract_type : ('r, 'c) spec -> ('r, 'c) spec

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.

val declare_seq : ?length:int gen -> ('r, 'c) spec -> ('r Seq.t, 'c Seq.t) spec

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.

val declare_affine_seq : 
  ?length:int gen ->
  ('r, 'c) spec ->
  ('r Seq.t, 'c Seq.t) spec

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 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.

Engine

Monolith's engine offers a very small number of operations. A typical usage scenario involves first calling declare once for each operation of the library under test, then invoking main so as to parse the command line and start the engine.

val declare : string -> ('r, 'c) spec -> 'r -> 'c -> unit

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 ^>>.

val main : ?prologue:(unit -> unit) -> int -> unit

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.

val dprintf : ('a, Buffer.t, unit) format -> 'a

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 ^>>.

exception PleaseBackOff

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.

exception Unimplemented

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.

Support

The submodule Support offers a number of useful functions. The name of these functions can appear in an error scenario printed by Monolith.

module Support : sig ... end

package monolith

Generating Data

Displaying Data and Code

Specifications

Engine

Support