package monolith

The submodule Gen offers facilities for generating values of many common types. It draws data from the file whose name is supplied on the command line. (If no file name is supplied, it draws random data from OCaml's Random module.)

The submodule Print offers a few facilities for printing OCaml values and expressions. It is meant to serve as a complement for the modules PPrint and PPrint.OCaml, which are part of the library pprint.

A value of type 'a code is a value of type 'a that is able to produce (on demand) a piece of OCaml code for itself. This code is represented as a string, which must form a valid OCaml expression (and must be surrounded with parentheses, if necessary).

The function code is a constructor for the type 'a code.

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

declare_concrete_type "t" declares a new concrete type named "t". This name is used in certain error messages. Which type 't is actually meant is inferred by the OCaml type-checker.

A concrete type is the same in the reference implementation and in the candidate implementation, which explains why the return type of this function is ('t, 't) spec.

The newly-declared type is not equipped with a generator; this can be done separately by using &&& or &&@. It is important to equip a concrete type with a generator (only) if this type is used to describe an input in a specification.

The newly-declared type may be equipped with an equality test, represented by the optional argument equal. If this argument is omitted, OCaml's polymorphic equality is used. It is important to equip a concrete type with an equality only if this type is used to describe an output in a specification. The newly-declared type may be equipped with a printer, represented by the optional argument print. This argument is required in almost all situations. As an exception, it can be omitted if this type describes an input and if this type is later equipped with a generator via &&@.

declare_abstract_type "t" declares a new abstract type named "t". This name is used in certain error messages. Which types 'r and 'c are actually meant, in the reference implementation and in the candidate implementation, is inferred by the OCaml type-checker.

An abstract type may be implemented in different ways in the reference implementation and in the candidate implementation, which explains why the return type of this function is ('r, 'c) spec. 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 newly-declared type may be equipped with a check function. This function is invoked by the system after every operation, and is applied to every data structure of type "t" that is currently at hand. The check function has access both to the reference data structure (the "model") and to the candidate data structure. It is expected to have no effect if all is well and to fail by raising Assertion_failure _ if something is wrong. It is up to the user to decide how much checking should be performed. Checking nothing at all is permitted. Checking that the candidate data structure seems well-formed is a common strategy. Checking that the candidate data structure is well-formed and is in agreement with its model is the most comprehensive check that can be performed.

The optional parameter var is a base name that is used for variables of type "t". If it is omitted, the first letter of the type's name is used.

The operator &&& equips a concrete type with a generator. In an application t &&& g, t should be a concrete type produced by declare_concrete_type, and g should be a generator for this type. Equipping a concrete type with a generator is required when this type is used to describe an input.

The operator &&@ equips a concrete type with a generator and (at the same time) with a printer for the generated values. In an application t &&@ g, the function g must have type unit -> 't code, which means that must be able to produce not only a value of type 't, but also, on demand, OCaml code for this value.

This feature can be used to declare an OCaml function type as a concrete type (thus working around the fact that a value of a function type cannot be printed).

unit represents the concrete type unit. It has been predeclared using declare_concrete_type.

bool represents the concrete type bool. It has been predeclared using declare_concrete_type.

int represents the concrete type int. It has been predeclared using declare_concrete_type. Unlike unit and bool, the specification int is not equipped with a generator, because it usually does not make sense to generate an integer in the huge interval [min_int, max_int]. Thus, if this type is used to describe an input, it must be equipped with a generator using &&& or &&@. To do so, one can also use one of the functions that follow; they are just int equipped with a suitable generator.

interval i j is int &&& Gen.interval i j.

interval_ i j is int &&& Gen.interval_ i j.

lt j is int &&& Gen.lt j.

le j is int &&& Gen.le j.

sequential() is int &&& Gen.sequential().

*** is the pair constructor. It is used to describe a pair (which typically appears as a function argument or result).

^^> is the arrow constructor. It is used to describe a function of one argument. By using it several times, one can also describe curried functions of several arguments, as is usual in OCaml.

^&> is the dependent arrow constructor. It is used to describe a function of one argument and give a name to this argument, which can be referred to in the codomain (the part of the specification that follows the operator ^&>). A typical example is the specification of a get function for a sequence: seq ^&> fun s -> lt (length s) ^^> int. Its 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 data structure s is built by the reference implementation, so the length function must be the one provided by the reference implementation.

% is the subset constructor. It is used to restrict the set of arguments that can be passed to an operation; in other words, it is used to express a precondition. For example, to express the fact that the operation pop must be applied to a nonempty stack, one would use nonempty % stack, where the function nonempty tests whether a (reference) stack is nonempty, and stack is the abstract type of stacks. This constructor currently cannot be applied to the result of an operation (where it would express a postcondition).

map specifies that a transformation must be applied to a value. The user must provide OCaml code for the transformation (in the form of a string) as well as the transformation itself, which in the reference implementation has type 'r1 -> 'r2 and in the candidate implementation has type 'c1 -> 'c2. The transformation can be applied to an output of an operation or to the operation itself, in which case the types 'r1, 'r2, 'c1, and 'c2 are function types. The transformation currently cannot be applied to an input.

The constructor nondet is used to annotate the result of an operation whose specification is nondeterministic. This indicates that several results are permitted; therefore, it does not make sense to ask the reference implementation for "the" expected result and to verify (via an equality test) that the candidate implementation produces the same result. Instead, in this case, the system runs the candidate implementation first, and asks the reference implementation to verify (by whatever appropriate means) that this result is permitted by the specification. For this reason, in this case, the reference implementation has type 'a postcondition instead of 'a. At this time, only a concrete type can be annotated with nondet.

declare name spec reference candidate declares the existence of an operation. Its parameters are the operation's name (used for printing), the operation's type and specification (represented by a runtime value of type ('r, 'c) spec), and the implementations of this operation in the reference and in the candidate (represented by values of type 'r and 'c).

main fuel is the main entry point. 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. The function prologue, if present, is run once at the beginning of each run; it is allowed to call data generation functions in the module Gen and can therefore set up the global parameters of the run, if desired.