linear only once the parameters are known. For example, our synthesizer accepts the following specification that decomposes an offset of a linear representation of a three-dimensional array with statically unknown dimensions into indices for each coordinate:

 

val (x1, y1, z1) = choose( (x: Int, y: Int, z: Int) Þ offset == x + dimX y + dimX dim Y z && 0 ≤ x && x < dimX && 0 ≤ y && y < dimY && 0 ≤ z && z < dimZ)

 

Here dimX, dim Y, dimZ are variables whose value is unknown until run-time. Note that the satisfiability of constraints that contain multiplications of variables is in general undecidable. In such parameterized case our synthesizer is complete in the sense that it generates code that ( 1) always terminates, ( 2) detects at run-time whether a solution exists for current parameter values, and ( 3) computes one solution whenever a solution exists.

In addition to integer arithmetic, other theories are amenable to synthesis and provide similar benefits. Consider the problem of splitting a set collection in a balanced way. The following code attempts to do that:

 

val (a1, a2) = choose( (a1:Set, a2:Set) Þ a1 union a2 == s && a1 intersect a2 == empty && a1.size == a2.size)

It turns out that for the above code our synthesizer emits a warning indicating that there are cases where the constraint has no solutions. Indeed, there are no solutions when the set s is of odd size. If we weaken the specification to

 

val (a1, a2) = choose( (a1:Set, a2:Set) Þ a1 union a2 == s && a1 intersect a2 == empty && a1.size − a2.size ≤ 1 && a2.size − a1.size ≤ 1)

then our synthesizer can prove that the code has a solution for all possible input sets s. The synthesizer emits code that, for each input, computes one such solution. The nature of constraints on sets is such that if there is one solution, then there are many solutions. Our synthesizer resolves these choices at compile time. The resulting generated code is therefore deterministic.

3. iMPLici T coMPu Ta Tions We next present programming language constructs that embed implicit computations into a general purpose programming language. Our constructs and algorithms are parametrized by a syntactically defined set Formulas. Formulas denote truth values, and we represent them as a well-defined subset of boolean-typed programming language expressions. Formulas are built from terms, denoted Terms, which are programming language expressions denoting values of certain types, such as integers or sets.

3. 1. The “choose” construct

As the basic form of supporting implicit computation, we
integrate into a programming language a construct of the
form
( 1)

3. 2. Generalized conditionals

Our next construct enables the developer to specify how to react to the absence of solutions to a constraint. As a concrete example, consider

given x Þ a = 2 ∗ x + 1 have x + 10 else a + 1

If a has value 7, then x is bound to 3 and the result is 13. If a is 10, the result is 11. The general form is the following:

given x Þ F have T else E

x is a bound variable, which may appear in both F and T. The boolean expression F belongs to Formulas, whereas T and E are any programming language expressions. The construct checks if there exists a value x satisfying F, and if so, computes T with x bound to one such value. If no such value exists, it computes E (which does not refer to x). The translation to guarded commands is again straightforward.

3. 3. expressive pattern matching

We can use the generalized conditionals to define an advanced form of pattern matching. Consider a pattern matching expression similar in structure to the example we