Information Technology Reference
In-Depth Information
(including for instance algebraic data types) can be encoded using this formalism.
In this context, generating values satisfying a predicate is framed as the
type inhab-
itation
problem, and the authors introduce the expression
elementof
T
to that end.
It is evaluated by invoking Z3 at run-time and is thus conceptually comparable to
our
find
construct but without support for recursive function unfolding. We have
previously found that recursive function unfolding works better as a mechanism
for satisfiability checking than using quantified axiomatization of recursive func-
tions [69]. In general, we believe that our examples are substantially more complex
than the experiences with
elementof
in the context of Dminor.
The ScalaZ3 library [38], used in Leon, integrates invocations to Z3 into a pro-
gramminglanguage.Becauseitisimplementedpurelyasalibrary,wewerethennot
able to integrate user-defined recursive functions and data types into constraints,
so the main application is to provide an embedded domain-specific language to ac-
cess the constraint language of Z3 (but not to extend it). A similar approach has
been taken by others to invoke the Yices SMT solver [20] from Haskell.
2
7.2 Synthesis of Functions
Our approach blends deductive synthesis [45,46,61], which incorporates transfor-
mation of specifications, inductive reasoning, recursion schemes and termination
checking, with modern SMT techniques and constraint solving for executable con-
straints. As one of our subroutines we include complete functional synthesis for
integer linear arithmetic [42] and extend it with a first implementation of complete
functional synthesis for algebraic data types [32,67]. This gives us building blocks
for synthesis of recursion-free code. To synthesize recursive code we build on and
further advance the counterexample-guided approach to synthesis [64].
Deductive synthesis frameworks.
Early work on synthesis [45, 46] focused on
synthesis using expressive and undecidable logics, such as first-order logic and
logic containing the induction principle.
Programming by refinement has been popularized as a manual activity [5,76].
Interactive tools have been developed to support such techniques in HOL [13].
A recent example of deductive synthesis and refinement is the Specware system
from Kesterel [61]. We were not able to use the system first-hand due to its
availability policy, but it appears to favor expressive power and control, whereas
we favor automation.
A combination of automated and interactive development is analogous to the
use of automation in interactive theorem provers, such as Isabelle [50]. However,
whereas in verification it is typically the case that the program is available, the
emphasis here is on constructing the program itself, starting from specifications.
Work on synthesis from specifications [65] resolves some of these diculties by
decoupling the problem of inferring program control structure and the problem
of synthesizing the computation along the control edges. The work leverages
verification techniques that use both approximation and lattice theoretic search
along with decision procedures, but appears to require more detailed information
about the structure of the expected solution than our approach.
