introduction

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.

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. They can then run our solver, which will find a solution to the given set of constraints (if one exists) and automatically update the heap to reflect the solution. Afterwards, the user can continue to manipulate the program heap in the usual imperative way.

Without a technology like this one, the standard solution would be to manually translate the problem into the language of an external solver, run the solver, and then again, manually translate the solution back to the native programming language. This obviously requires more work, it is cumbersome, and after all, it is more error-prone.

architecture

arch
  1. serialize the heap into relations
  2. translate specs and heap relations into Kodkod
  3. translate relational into boolean logic
  4. (if a solution is found) restore relations from boolean assignments
  5. (if a solution is found) restore field values from relations
  6. (if a solution is found) restore the heap to reflect the solution

applications

  • solving hard constraint problems; puzzles (sudoku, n-queens, knight's tour, ...), graph problems (k-coloring, hamiltonian path, max clique, ...), schedulers, dependency mangers, ...
  • test input generation; e.g. generate data structure instances that satisfy complex constraints
  • specification validation; specifications can also contain errors, and the most intuitive way to test a specification would be to execute it on some concrete input and see if the result makes sense or not
  • runtime assertion checking; check whether a given rich property holds at an arbitrary point during the execution of a program

limitations

  • boundedness; everything has to be bounded, i.e. Squander cannot generate an arbitrary number of new objects (which may be needed to satisfy a specification); instead, the exact number of new objects of each class must be specified by the user
  • small integers; integers must also be bounded to a small bitwidth (to make the solving tractable), which can occasionally cause subtle integer overflow bugs, which are typically hard to find
  • equality issues; referential equality is used by default for all classes except for String, so it is impossible to write a spec that asserts that two objects are equal in the sense of Java equals
  • lack of support for higher-order expressions; it is not possible to write a specification that says “find a path in the graph such that there is no other path in the graph longer than it” and solve it with Squander; it is possible, however, to express and solve “find a path in the graph with at least k nodes”, which is computationally as hard as the previous problem, because a binary search can be used to efficiently find the maximum k for which a solution exists