Note: Mica is a research prototype and should not be used in production code. (We have made Mica available on Opam so that others may try it out & contribute to Mica if they wish.) Please contact Ernest Ng (ernest@cs.cornell.edu
) if you'd like to contribute to Mica or have any questions!
Mica is a PPX extension that automates differential testing for a pair of OCaml modules implementing the same signature. Users annotate module signatures with the directive [@@deriving mica]
, and at compile-time, Mica derives specialized property-based testing (PBT) code that checks if two modules implementing the signature are observationally equivalent. (Under the hood, Mica uses Jane Street's Core.Quickcheck
PBT library.)
Mica was presented at the OCaml Workshop '24 and the ICFP '23 SRC. The OCaml Workshop paper contains a lot more details about Mica's design -- this README focuses on describing how to interact with our OCaml artifact.
An simple webapp demonstrating Mica is available here.
Mica is available on opam. To install, run:
opam update
opam install ppx_mica
(Note that OCaml 5.1 or newer is required.)
To use Mica, add ppx_mica
, ppx_deriving.show
and ppx_jane
to the preprocess
field in your dune
file. (Mica produces code that uses ppx_deriving
and ppx_jane
under the hood, so these two PPXes are also required in order for the code produced by Mica to compile.)
(library
...
(preprocess (pps ppx_mica ppx_deriving.show ppx_jane)))
Here is how we envisage users interacting with Mica:
Suppose modules M1
& M2
both implement the module signature S
. Users insert the directive [@@deriving_inline mica]
beneath the definition of S
, like so:
module type S = sig
type 'a t
val empty : 'a t
val add : 'a -> 'a t -> 'a t
...
end
[@@deriving_inline mica]
...
[@@@end]
Then, after users run dune build --auto-promote
, the derived PBT code is automatically inserted in-line in the source file in-between [@@deriving_inline mica]
and [@@@end]
. (Note: this doesn't work fully out of the box at the moment -- see compilation notes for details.)
Then, after running dune build
, Mica derives the following PBT code:
module Mica = struct
(** [expr] is an inductively-defined algebraic data type
representing {i symbolic expressions}.
Each [val] declaration in the module signature [S] corresponds to a
cosntructor for [expr] that shares the same name, arity & argument types.
- Type variables ['a] are instantiated with [int]
- Function arguments of type ['a t] correpond to
constructor arguments of type [expr] *)
type expr =
| Empty
| Is_empty of expr
...
[@@deriving show, ...]
(** Types of symbolic expressions *)
type ty = Int | IntT | ... [@@deriving show, ...]
(** QuickCheck generator for symbolic expressions.
[gen_expr ty] generates random [expr]s of type [ty]. *)
let rec gen_expr : ty -> Core.Quickcheck.Generator.t = ...
(** Functor that interprets symbolic expressions *)
module Interpret (M : S) = struct
(** Values of symbolic expressions *)
type value = ValInt of int | ValIntT of int M.t | ...
(** Big-step interpreter for symbolic expressions:
[interp] takes an [expr] and interprets it over the module
[M], evaluating the [expr] to a [value] *)
let rec interp : expr -> value = ...
end
(** Functor that tests [M1] and [M2] for observational equivalence *)
module TestHarness (M1 : S) (M2 : S) = struct
(* Runs all observational equivalence tests *)
let run_tests : unit -> unit = ...
end
end
M1
and M2
both implement S
. To run Mica's testing code and check whether M1
& M2
are observationally equivalent with respect to S
, one can invoke the run_tests : unit -> unit
function in Mica's TestHarness
functor, like so:module T = Mica.TestHarness(M1)(M2)
let () = T.run_tests ()
int
, string option
), and not abstract types defined in a module (e.g. 'a M.t
), since abstract types have a more abstract notion of equality different from OCaml's standard notion of polymorphic equality.At the moment, Mica only works with module signatures that define one abstract type (e.g. t
or 'a t
) and only contain pure functions. Modules with multiple abstract types and/or abstract types with multiple type parameters are not supported at the moment.
There is a known issue with Ppxlib (#338, #342) which causes Ppxlib to error when Dune is promoting changes (i.e. after one runs dune build --auto-promote
, during which Dune inserts the code derived by Mica into the source file).
To fix this issue, remove [@@deriving_inline mica]
and [@@@end]
from the source file while keeping the code inserted by Dune/Mica. Then, recompile by running dune build again
. This second compilation run should complete successfully!
Code for the following case studies (along with the code automatically derived by Mica) is located in the ancillary mica_case_studies
repo.
We have tested Mica with the following module signatures, each of which is implemented by two different modules:
Base.Queue
& Base.Linked_queue
) (link)stdint
and ocaml-integers
libraries) (link)charset
library & the standard library's Set.Make(Char)
module) (link)For more details regarding these case studies, we refer the reader to the mica_case_studies
repo as well as the OCaml Workshop paper.