Mica: Automated Differential Testing for OCaml Modules

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 online demo of Mica is available here.

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

• Now suppose modules 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 ()

• Note: Mica only tests for observational equivalence at concrete types (e.g. 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.

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:

• Finite Sets (lists & Binary Search Trees) (link)
• Regular Expression Matchers (Brzozowski Derivatives & Deterministic Finite Automata) (link)
• Polynomials (Horner schema & monomial-based representations) (link)
• Ephemeral Queues (Base.Queue & Base.Linked_queue) (link)
• Unsigned integer arithmetic (the stdint and ocaml-integers libraries) (link)
• Character sets (the charset library & the standard library's Set.Make(Char) module) (link)
• Persistent maps (red-black trees & association lists) (link)
• John Hughes's How to Specify It (catching bugs in BST implementations) (link)
• UPenn CIS 1200 student homework submissions (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.