Download Now Free registration required
Synthesis of program fragments from specifications can make programs easier to write and easier to reason about. The authors present Comfusy, a tool that extends the compiler for the general-purpose programming language Scala with (non-reactive) functional synthesis over unbounded domains. Comfusy accepts expressions with input and output variables specifying relations on integers and sets. Comfusy symbolically computes the precise domain for the given relation and generates the function from inputs to outputs. The outputs are guaranteed to satisfy the relation whenever the inputs belong to the relation domain. The core of their synthesis algorithm is an extension of quantifier elimination that generates programs to compute witnesses for eliminated variables.
- Format: PDF
- Size: 143.73 KB