Information Technology Reference
In-Depth Information
interesting to understand to what extend such complete specifications change the
software development process. Writing data structures using constraints shows
the productivity advantages of using constraints, because data structure invari-
ants are reusable across all operations, whereas the remaining specification of
each individual operation becomes extremely concise. The development process
thus approaches the description of a data structure design from a textbook [15],
which starts from basic invariants and uses them as guiding principle when pre-
senting the implementation of data structure operations. We are thus hopeful
that, among other results, we can soon enable automated generation of ecient
unbounded data structures from high-level descriptions, analogously to recent
breakthrough on cache coherence protocol generation [71].
An exciting future direction is to use run-time property verification tech-
niques to eciently combine code generated through speculative synthesis and
constraint solving. In many synthesis approaches, due to a heavy use of example-
driven techniques and the limitations of static verification, it is also quite possible
that the automatically generated implementation is incorrect for some of the in-
puts. In such cases, techniques of run-time verification can be used to detect,
with little overhead, the violation of specifications for given inputs. As a result,
synthesis could be used to generate fast paths and likely code fragments, while
ensuring the overall adherence to specification at run time.
In general, we are excited about future interplay between dynamic and static
approaches to make specifications executable, which is related to partial evalu-
ation and to techniques for compilation of declarative programming languages,
as well as static optimization of run-time checks.
7 Related Work
We provide an overview of related work on executing constraints using general-
purpose solvers at run-time, synthesizing constraints into conventional functional
and imperative code, and combining these two extreme approaches by staging
the computation between run-time and compile time.
7.1 Run-Time Constraint Solving
This proceedings volume contains a notable approach and tool Boogaloo [56],
which enables execution of a rich intermediate language Boogie [43]. The orig-
inal purpose of Boogie is static verification [6]. The usual methods to verify
Boogie programs generate conservative sucient verification, which become un-
provable if the invariants are not inductive. Tools such as Boogaloo complement
verification-condition generation approaches and help developer distinguish er-
rors in programs or specifications that would manifest at run-time from those
errors that come from inductive statements not being strong enough. A run-
time interpreter for the annotations of the Jahob verification system [79] can
also execute certain limited form of specifications, but does not use symbolic ex-
ecution techniques and treats quantifiers more conservatively than the approach
 
Search WWH ::




Custom Search