package monolith

Changes

2024/11/26

• The documentation of the specification combinators has been re-organized in sections and subsections. Finding the desired combinator should now be easier.

• The new combinator naive_array offers limited support for arrays.

• The new combinator naive_seq offers limited support for sequences (that is, for the type constructor Seq.t).

• The new combinator pair is a synonym for ( *** ).

• The new combinator triple offers support for triples.

• The new combinator either offers support for the type constructor Either.t.

• The new combinators iter, foldr, foldl, iteri, foldri, foldli offer support for iteration functions.

• An unintentional and undocumented limitation has been fixed: so far, uses of the combinator map_into would work only at the root of the specification or in the right-hand side of an arrow ^>. It should now be possible to use map_into under other combinators that expect a deconstructible specification, such as ^!> (in the right-hand side), ( *** ), option, result, list, etc. This improvement affects not only map_into, but also a number of other combinators that are defined in terms of map_into.

• Monolith now requires OCaml 4.12 or later.

• In Makefile.monolith,

  • the default switch is changed from 4.11.1 to 4.14.2; this can be overridden by defining SWITCH;

  • make test automatically disables the MacOS crash reporter;

  • the use of ulimit -s is abandoned.

2023/06/04

• Fix a bug in Gen.with_source where a file descriptor was not properly closed, causing Monolith to eventually run out of descriptors. (Contributed by Samuel Hym.)

• Fix a minor bug that could cause an assertion failure while printing an error scenario.

• Fix a bug in Makefile.monolith that would cause make test to launch multiple instances of dune in parallel and therefore to fail.

• Remove the use of Obj.magic in module Tag.

2021/05/25

• Fix a bug where the exception PleaseBackOff was unintendedly caught by the combinator ^!> and therefore did not work as intended. (Reported and fixed by Nicolas Osborne.)

2020/10/26

• The functions declare_concrete_type, &&& and &&@ disappear. They are replaced with two new combinators, constructible and deconstructible. The combinator ifpol (described further on) can be used to construct a specification that is both constructible and deconstructible. The idiom int &&& range is replaced with int_within range.

• The function declare_abstract_type no longer requires the type's name as an argument; it takes a unit argument instead.

• The arrow combinator ^^> is renamed ^>. The dependent arrow combinator ^&> is renamed ^>>.

• New specification combinator ^!>. This combinator describes a function that can raise an exception, and requires the reference implementation and the candidate implementation to raise exactly the same exception.

• New specification combinator ^?>. This combinator describes a nondeterministic function. spec1 ^?> spec2 is a short-hand for spec1 ^> nondet spec2.

• New specification combinator ^!?>. This combinator describes a function that can raise an exception, and can decide in a nondeterministic way whether it wishes to raise an exception and what exception it wishes to raise. The reference implementation is allowed to observe this behavior and to react accordingly.

• New specification combinators ^!>>, ^?>>, and ^!?>>. These are the dependent variants of the previous three combinators.

• New specification combinators option, result, and list. These combinators make it easy to describe an operation that expects or returns an option, a result, or a list.

• New specification combinator declare_seq. This (effectful) combinator makes it relatively easy to describe an operation that expects or returns a sequence.

• New specification combinator map_into. This combinator is typically used to wrap an operation or to transform the result of an operation.

• New specification combinator map_outof. This combinator is typically used to construct an argument to an operation via a transformation.

• Removed the combinator map, whose type was fishy.

• New specification combinators rot2 and rot3. (rot2 is also known as flip.) These combinators move a distant argument to the front. This is useful when a dependency between arguments runs contrary to the order of the arguments. These combinators can be used only in a positive position.

• New specification combinators curry and uncurry. These combinators transform a function that expects a pair into a function that expects two separate arguments, and vice-versa. These combinators can be used only in a positive position.

• New specification combinator ignored. This combinator is used to describe the output (or part of the output) of an operation, and indicates that this output should be ignored.

• Changed the type of the specification combinator nondet. Removed the limitation that this combinator can be applied only to a concrete type.

• New specification constant exn. The new function override_exn_eq allows overriding the notion of equality that is associated with the concrete type exn. This is useful when the reference implementation and candidate implementation raise different exceptions.

• New specification combinator ifpol, which allows distinguishing between negative and positive occurrences in a specification. This low-level combinator can be useful in the definition of higher-level abstractions.

• New specification combinator fix, which allows building recursive specifications.

• New specification combinator abstract, which declares an abstract type on the fly, together with a conversion operation out of this abstract type to its concrete definition. This can be used to deal with functions that return functions.

• New exception PleaseBackOff, which the reference implementation is allowed to raise when an operation (or some particular case of an operation) is illegal or is not implemented. This causes the Monolith engine to silently ignore this scenario. No side effects must be performed by the reference implementation before raising this exception.

• New exception Unimplemented, which the candidate implementation is allowed to raise when an operation (or some particular case of an operation) is not implemented. This causes the Monolith engine to silently ignore this scenario.

• New definition of the type 'a code as a synonym for 'a * appearance. New constructors for the type appearance, including constant, document, and infix.

• The functions interval and interval_ are renamed semi_open_interval and closed_interval.

• Significant internal changes, leading to simpler and possibly faster code.

• The file Makefile.monolith is now installed with the library, so it need no longer be copied into one's project, unless one wishes to adapt it.

• In Makefile.monolith, new entries make multicore and make tmux, both of which implement parallel fuzzing with multiple afl-fuzz processes.

• In Makefile.monolith, new entry make random, which implements random testing.

• On 64-bit machines, the function bits did not generate the full range of 63-bit integers; it was inadvertently limited to 32-bit integers. A number of other functions that depend on it, such as interval, were also wrong. Fixed (hopefully).

2020/06/09

• Initial release.