Information Technology Reference
In-Depth Information
contracts is done using heuristically guided injection of (sequences of) routine
calls into predefined code templates.
Our synthesis approach works with purely functional programs and does not
depend on characterization of program behavior. It is more general in the sense
that it focuses on synthesizing whole correct functions from scratch and does
not depend on already existing code. Moreover, rather than using execution of
tests to define starting points for synthesis and SMT solvers just to guide the
search, our approach utilizes SMT solvers to guarantee correctness of generated
programs and uses execution of tests to speedup the search. Coupling of flexible
program generators and the Leon verifier provides more expressive power of the
synthesis than filling of predefined code schemas.
7.3 Combining Run-Time and Compile-Time Approaches
We have argued that constraint solving generalizes run-time checking, and allows
the underlying techniques to be applied in more scenarios than providing addi-
tional redundancy. The case of optimizing run-time checks also points out that
there is a large potential for speedups in executing specifications: in the limit,
a statically proved assertion can be eliminated, so its execution cost goes from
traversing a significant portion of program state to zero. As is in general the case
for compilation, such static pre-computation can be viewed as partial evaluation,
and has been successfully applied for temporal finite-state properties [10].
Compilation and transformation of logic programs.
Compilation of logic pro-
grams is important starting point for improving the baseline of compiled code.
A potential ineciency in the current approach (though still only a polynomial
factor) is that the constraint solver and the underlying programming language
use a different representation of values, so values need to be converted at the
boundary of constraints and standard functional code. Techniques such as those
employed in Warren's Abstract Machine (WAM) is relevant in this context [1].
Deeper optimizations and potentially exponential speedups can be obtained us-
ing tabling [14], program transformation [59] and partial evaluation [12,25].
Specifications as a fallback to imperative code.
The idea to use specifications as a
fall-back mechanism for imperative code was adopted in [57]. Dynamic contract
checking is applied and, upon violations, specifications can be
executed
.Thetech-
nique ignores the erroneous state and computes output values for methods given
concrete input values and the method contract. The implementation uses a rela-
tional logic similar to Alloy [31] for specifications, and deploys the Kodkod model
finder [70]. A related tight integration between Java and the Kodkod engine is pre-
sented in [48]. We expect that automated synthesis will allow the developers to use
specifications alone in such scenarios, with a candidate implementation generated
automatically.
Data structure repair.
It is worth mentioning that this proceedings also con-
tains new results [78] in the exciting area of
data structure repair
. This general
approach is related to solving constraints at run-time. The assumption in data
structure repair is that, even if a given data structure does not satisfy the desired
