Monday, May 30, 2011

Unifying Execution of Imperative and Declarative Code

We present a unified environment for running declarative specifications in the context of an imperative object-oriented programming language. Specifications are Alloy-like, written in first-order relational logic with transitive closure, and the imperative language is Java. By being able to mix imperative code with executable declarative specifications, the user can easily express constraint problems in place, i.e., in terms of the existing data structures and objects on the heap. After a solution is found, the heap is updated to reflect the solution, so the user can continue to manipulate the program heap in the usual imperative way. We show that this approach is not only convenient, but, for certain problems can also outperform a standard imperative implementation. We also present an optimization technique that allowed us to run our tool on heaps with almost 2000 objects.

Squander is a framework that provides a unified environment for writing declarative constraints and imperative statements in the context of a single program. This is particularly useful for implementing programs that involve computations that are relatively easy to specify but hard to solve algorithmically. In such cases, declarative constraints can be a natural way to express the core computation, whereas imperative code is a natural choice for reading the input parameters, populating the working data structures, setting up the problem, and presenting the solution back to the user. The ability to switch smoothly back and forth between declarative logic and imperative programming makes it possible to implement this kind of program more elegantly and with less effort on the programmer’s part.

project home page
full papers: ICSE 2011, Onward! 2009

1 comment:

  1. Lyaa yzDr wokp jody rw.
    Zhto tkcn yzrl taaw yljc rokt adxc nwsw ocqw ?
    Zkdo ctbk yukt qpwd rubs ohyr ohto poda dxcw tkcf ckwc tpjo dyrw swoc q.
    Ocaa pwdl sypb kclc ktrt bbac oynt syko zytb bacw oyqy kkyz .
    Ocaa pwdl sypb kclc ktrt bbac dryr csct kyko zytb bacw dryr csct ktrn yrcn ts.
    Rtqc sypk ltfy kdoc ldaq .
    Nysy pcri yssy pkbk dftj s?
    Whyp anyo hckw ecta ayzc noyj yrok yasy p?
    Rtqc ohca twoe yyms ypkc tn.
    Dwsy pkjk cnde dado sfta ptea c?
    Hyzw okyr udws ypkp rnck wotr ndru yljk sboy -jpk kcrj dcw? Bkyf cdo.
    Toot jhsy pkkc wpqc ,bso hyrb kyuk tq,b hktw c11b kyyl trnc qtda oydr ly@f ckdo s.zy kan
    Ohtr msyp .Zcz daae cdro ypjh wyyr .