COMFUSY: COMplete FUnctional SYnthesis
Comfusy is a tool for synthesizing executable code from specifications in linear integer arithmetic and constraints on sets of objects.
- see PLDI 2010 Paper for the description of this work
Comfusy works as a plugin for the Scala compiler. Comfusy was developed and tested with the version 2.7.7 of Scala (*not* the more recent 2.8.* or 2.9.* releases).
- The source code is available on GitHub for the brave.
- Browse through the examples here: examples
Using Synthesis to Generate and Compile Code
(The following assumes that the plugin Jar file is called
synthesis-plugin.jar and is in the current directory.)
- Compile your code with
scalac -Xplugin:synthesis-plugin.jar -classpath synthesis-plugin.jar YourFile.scala
- Run your code with
scala -classpath synthesis-plugin.jar YourObject
Using Synthesis in the Interpreter
You can also use the plugin in the Scala interpreter (REPL) directly. Start
scala -Xplugin:synthesis-plugin.jar -classpath synthesis-plugin.jar
then try for instance:
scala> val answer = choose((x: Int) => x > 41)
…and you will get:
<console>:7: Synthesis predicate has multiple solutions for variable assignment: Solution 1: x = 42 Solution 2: x = 43 val answer = choose((x: Int) => x > 41) ^ answer: Int = 42
Notes on using Z3 for additional compile-time checks
By default, the plugin tries to run Z3 to check that calls to the
choose function have a (unique) solution, and warns the user if this is not always the case (the warnings include counter-examples). It also checks if pattern-matching expressions are exhaustive (no input value can fall through all the cases), and if all cases are reachable (no case is subsumed by the cases above it).
* The command the plugin tries to run is
z3 -smt -m -in, so make sure Z3 is in the path and that it accepts these arguments (this may depend on the version you have). We currently do not support any other solver.
* You can disable these checks by compiling the code with the command:
scalac -Xplugin:synthesis-plugin.jar -classpath synthesis-plugin.jar -P:synthesis:nowarnings YourFile.scala
(Comfusy parses Z3 models to produce a warning; versions of Z3 more recent than 2.18 may not output the proper format.)