An imperative extension to alloy and a compiler for its execution

This thesis presents an extension of the Alloy specification language with the standard imperative programming constructs, allowing for the natural specification of dynamic systems. Using this extension, programmers can express stateful behavior directly, mixing declarative and imperative styles as desired. A relational semantics for the new imperative constructs will ensure that specifications written using the extension are translatable into the original Alloy language, allowing their analysis using the existing Alloy Analyzer. The thesis also presents a compiler from the extended Alloy language to Prolog so that specifications may be efficiently executed. While the Alloy Analyzer's SAT-based analysis engine is incredibly fast in exploring a wide search tree, Prolog's unification-based strategy has the ability to delve very deeply into highly constrained search trees. Many specifications of dynamic systems have this property, making Prolog a perfect engine for executing them. This combination of a language extension and a compiler for its execution represents an end-to-end solution for programming. The Alloy Analyzer allows the programmer to check properties of a high-level specification of the desired behavior, and the Prolog-based compiler allows the execution of that specification; if the compiled program is not fast enough, the programmer may refine the specification to make it faster, and the Alloy Analyzer will check that the refinement step has not introduced errors.

Department dc:contributor.department

Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science.

Grantor dc:publisher

Massachusetts Institute of Technology

Year dc:date.issued

2010

Author dc:creator

• Near, Joseph P. (Joseph Paul)

Advisor dc:contributor.advisor

• Daniel Jackson.

• Electrical Engineering and Computer Science.

Statement dc:rights

• M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission.

Licence dc:rights.uri

• http://dspace.mit.edu/handle/1721.1/7582

Language dc:language.iso

eng

Handle dc:identifier.uri

http://hdl.handle.net/1721.1/60178

OAI identifier oai:identifier

oai:dspace.mit.edu:1721.1/60178