Information Technology Reference
In-Depth Information
Executing Specifications
Using Synthesis and Constraint Solving
Viktor Kuncak 1 , Etienne Kneuss 1 , and Philippe Suter 1 , 2
1 Ecole Polytechnique Federale de Lausanne (EPFL), Switzerland
2 IBM T.J. Watson Research Center, Yorktown Heights, NY, USA
{ firstname.lastname } @epfl.ch , psuter@us.ibm.com
Abstract. Specifications are key to improving software reliability as
well as documenting precisely the intended behavior of software. Writing
specifications is still perceived as expensive. Of course, writing imple-
mentations is at least as expensive, but is hardly questioned because
there is currently no real alternative. Our goal is to give specifications
a more balanced role compared to implementations, enabling the devel-
opers to compile, execute, optimize, and verify against each other mixed
code fragments containing both specifications and implementations. To
make specification constructs executable we combine deductive synthe-
sis with run-time constraint solving, in both cases leveraging modern
SMT solvers. Our tool decomposes specifications into simpler fragments
using a cost-driven deductive synthesis framework. It compiles as many
fragments as possible into conventional functional code; it executes the
remaining fragments by invoking our constraint solver that extends an
SMT solver to handle recursive functions. Using this approach we were
able to execute constraints that describe the desired properties of inte-
gers, sets, maps and algebraic data types.
1 Introduction
Specifications are currently second class citizens in software development. An
implementation is obligatory; specification is optional. Our goal is to assign to
specifications a more balanced role compared to implementations. For this to
happen, we aim to allow developers to execute specifications, even if such exe-
cution is slower or less predictable than execution of imperative and functional
code. We wish to permit developers to write mixed code fragments containing
both specifications and implementations. They should be able to compile, exe-
cute, optimize, and verify such fragments against each other.
By execution of specifications we mean not only testing whether a constraint
is true for known values of variables (as when checking e.g. assertions), but
also computing a missing value so that the given constraint is satisfied. Such
constraint solving functionality can also be thought as one way of automating
 
Search WWH ::




Custom Search