WG211/M10Rayside

Synthesizing Imperative Code from Relational Specifications by Derek Rayside

We are exploring techniques to synthesize imperative (Java) code from specifications written in a relational logic (Alloy). We intend to discuss two approaches:

1. A syntax-directed translation from a subset of Alloy that we call "navigable expressions" to Java iterators. We discussed an earlier version of this work at the IFIP 2.11 meeting in Waterloo last December. Since then we have re-implemented the system in MetaAspectJ and seen great performance improvements. We have also conducted a user study examining programmer productivity with our system versus plain Java.

2. Preliminary work on a constraint-solving based synthesis approach that generates imperative implementations of heap manipulating procedures based on their specifications. We have been exploring these ideas in the context of binary tree operations such as containment, insertion, and deletion. This work is at a very early stage.