Mica: Automated Differential Testing for OCaml Modules

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!

Overview

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.

Installation

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

Using Mica

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
module T = Mica.TestHarness(M1)(M2)
let () = T.run_tests ()

Limitations

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.

Compilation notes

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!

Case Studies

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:

For more details regarding these case studies, we refer the reader to the mica_case_studies repo as well as the OCaml Workshop paper.