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.

翻译：假设我们有两个实现相同签名的OCaml模块。如何检查它们是否具有观测等价性——即它们在所有输入上的行为是否一致？一种成熟的技术是使用基于属性的测试（PBT）工具，如QuickCheck。然而，目前这种方法可能需要大量样板代码和临时测试框架。为解决此问题，我们提出了Mica，一个用于测试OCaml模块观测等价性的自动化工具。Mica被实现为PPX编译器扩展，允许用户在模块签名中提供最小化注解。这些注解引导Mica自动生成用于检查观测等价性的专用PBT代码。我们讨论了Mica的设计，并通过从真实世界OCaml库中选取的多个模块展示了其作为测试工具的有效性。