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).

• You can download the .jar file of the plugin here: synthesis-plugin.jar (older version: synthesis-plugin-older.jar, without support for parametrized linear integer arithmetic).

• The source code is available on GitHub for the brave.

• Browse through the examples here: examples

(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

You can also use the plugin in the Scala interpreter (REPL) directly. Start scala with:

scala -Xplugin:synthesis-plugin.jar -classpath synthesis-plugin.jar

then type:

import synthesis.Definitions._

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

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.)

Comfusy has been used to synthesize a part of computation used to generate the following Happy New Year 2010 Video (see the making-of at 0:47).

The people involved in the development of Comfusy are, in alphabetical order: Viktor Kuncak, Mikaël Mayer, Ruzica Piskac and Philippe Suter.