Synthesizing Layout Engines From Relational Specifications
Thibaud Hottelier, Rastislav Bodík, James Ide, Doug Kimelman · 2011
We develop algorithms for expressing, verifying and implementing document layout languages. To simplify specification and enable reuse of components, we use relational specifications. Relying on relations, rather than on functions, we free the designer from having to reason about the mechanics of how the layout will be computed. We verify layout languages by proving that all documents in the language will have unambiguous layout. To ease implementation of layout languages, we synthesize a fast propagation layout engine. Our approach relies on recent work for synthesizing functions from relations. We extend the work by making the synthesizer modular, improving scalability when the relational constraint system is naturally modular. We show empirically that layout languages are modular, but our modular synthesizer may be applicable also in other domains. We validate the algorithms on three case studies.