Mica: Automated Differential Testing for OCaml Modules

TL;DR

Mica is an automated tool that simplifies the process of testing observational equivalence of OCaml modules by generating property-based tests with minimal user annotations.

Contribution

Mica introduces a PPX extension that automatically derives property-based tests for OCaml modules, reducing boilerplate and manual effort.

Findings

Successfully tested real-world OCaml modules

Reduced manual coding in equivalence testing

Demonstrated effectiveness of Mica in practical scenarios

Abstract

Suppose we are given two OCaml modules implementing the same signature. How do we check that they are observationally equivalent -- that is, that they behave the same on all inputs? One established technique is to use a property-based testing (PBT) tool such as QuickCheck. Currently, however, this can require significant amounts of boilerplate code and ad-hoc test harnesses. To address this issue, we present Mica, an automated tool for testing observational equivalence of OCaml modules. Mica is implemented as a PPX compiler extension, allowing users to supply minimal annotations to a module signature. These annotations guide Mica to automatically derive specialized PBT code that checks observational equivalence. We discuss the design of Mica and demonstrate its efficacy as a testing tool on various modules taken from real-world OCaml libraries.