FROM RELATIONAL SPECIFICATIONS TO LOGIC PROGRAMS
This paper presents a compiler from expressive, relational specifications to logic programs. Specifically, the compiler translates the Imperative Alloy specification language to Prolog. Imperative Alloy is a declarative, relational specification language based on first-order logic and extended with imperative constructs; Alloy specifications are traditionally not executable. In spite of this theoretical limitation, the compiler produces useful prototype implementations for many specifications. 1. Introduction This paper presents a compiler from declarative, relational specifications to Prolog programs, eliminating the need for manual implementation. I express specifications in Im- perative Alloy [28], a language based on the combination of first-order logic with transitive closure and the standard imperative programming constructs. My compiler transforms these specifications to Prolog for execution. Prolog represents an appropriate target lan- guage, since it supports nondeterminism and provides a database for storing global relations; the compiler uses these features to simulate Alloy’s relational operators, quantifiers, and classical negation. The existing Alloy Analyzer is designed for the verification and animation of specifi- cations. My compiler is intended to complement the Analyzer by executing specifications. Animators perform their analyses within a fixed universe of predetermined size, while ex- ecution engines allow the creation of new objects. In practice, animators typically deal with models containing tens of objects, while execution engines must handle hundreds or thousands. In this case, this increased scalability comes at the cost of analysis: the Alloy Analyzer is designed to check all cases within a small bound, while my compiler executes a single, potentially large, case. In exchange, the compiler provides eciency: most specifi- cations can be executed fast enough to serve as prototype implementations. Along with the Alloy Analyzer, my compiler provides end-to-end support for speci- fying and implementing programs. The Alloy language provides the expressive logic and relational constructs needed to express complex properties of programs and data; the An- alyzer supports the animation and verification of program specifications; and the compiler presented in this paper allows for the ecient execution of those specifications.
Free download research paper
CSE PROJECTS