Welcome to the documentation page for our automated PBT tool, Mica!
Mica parses any generic OCaml module signature, and checks whether two modules implementing the signature are observationally equivalent by generating random sequences of commands using Core.QuickCheck.
This project compiles with dune build.
dune exec -- mica [.ml/.mli file containing signature] [.ml file containing 1st module] [.ml file containing 2nd module]
This command runs Mica and creates two new files:
lib/Generated.ml (contains PBT code for testing an OCaml module)bin/compare_impls.ml (code for an executable that tests two modules for observational equivalence) To run the generated executable, run dune exec -- compare_impls.(Note: The name of the module signature must be the same as the .ml/.mli file it is contained within.)
To run Mica on SetInterface, a module signature for finite sets, and check if two modules ListSet and BSTSet implementing this signature are observationally equivalent, we can run: dune exec -- mica lib/sets/SetInterface.ml lib/sets/ListSet.ml lib/sets/BSTSet.ml
This checks if the ListSet and BSTSet modules both correctly implement the interface SetInterface. The files lib/GeneratedSetPBTCode.ml and bin/GeneratedSetExecutable.ml in the GitHub repo contain PBT code that is automatically generated by Mica.