Mica Case Studies

This repo contains case studies for Mica, a PPX that automates differential testing for OCaml modules. A simple webapp demonstrating Mica (using the case studies in this repo) is available here.

The main Mica repo contains more details on Mica.

For each example (where possible), we have included an executable which runs the PBT code automatically produced by Mica.

Here are the case studies:

• Finite Sets (lists & BSTs) (link)
  • Executable: Run dune exec -- mica_sets
• Regular Expression Matchers (Brzozowski Derivatives & DFAs) (link)
  • Executable: Run dune exec -- mica_regexes
• Polynomials (Horner schema & monomial-based representations) (link)
  • Executable: Run dune exec -- mica_polynomials
• Ephemeral Queues (Base.Queue & Base.Linked_queue) (link)
  • Executable: Run dune exec -- mica_queues
• Unsigned integer arithmetic (the stdint and ocaml-integer libraries) (link)
  • Executable: Run dune exec -- mica_unsigned_ints
• Character sets (the charset library & the standard library's Set.Make(Char) module) (link)
  • Executable: Run dune exec -- mica_charsets
• Persistent maps (red-black trees & association lists) (link)
  • Executable: Run dune exec -- mica_maps
• John Hughes's How to Specify It (catching bugs in BST implementations) (link)
  • Executable: Run dune exec -- mica_how_to_specify_it (note: the executable will terminate after finding the first bug)
• UPenn CIS 1200 student homework submissions (link)
  • Note: no executable is available for this case study (to avoid posting homework solutions online)