An imperative extension to alloy and a compiler for its execution
Thesis (S.M.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2010.
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | eng |
| Published: |
Massachusetts Institute of Technology
2010
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/1721.1/60178 |
| _version_ | 1826199841814872064 |
|---|---|
| author | Near, Joseph P. (Joseph Paul) |
| author2 | Daniel Jackson. |
| author_facet | Daniel Jackson. Near, Joseph P. (Joseph Paul) |
| author_sort | Near, Joseph P. (Joseph Paul) |
| collection | MIT |
| description | Thesis (S.M.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2010. |
| first_indexed | 2024-09-23T11:26:37Z |
| format | Thesis |
| id | mit-1721.1/60178 |
| institution | Massachusetts Institute of Technology |
| language | eng |
| last_indexed | 2024-09-23T11:26:37Z |
| publishDate | 2010 |
| publisher | Massachusetts Institute of Technology |
| record_format | dspace |
| spelling | mit-1721.1/601782019-04-12T16:02:00Z An imperative extension to alloy and a compiler for its execution Near, Joseph P. (Joseph Paul) Daniel Jackson. Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science. Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science. Electrical Engineering and Computer Science. Thesis (S.M.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2010. Includes bibliographical references (p. 50-52). 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. by Joseph P. Near. S.M. 2010-12-06T17:34:05Z 2010-12-06T17:34:05Z 2010 2010 Thesis http://hdl.handle.net/1721.1/60178 681903386 eng 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. http://dspace.mit.edu/handle/1721.1/7582 52 p. application/pdf Massachusetts Institute of Technology |
| spellingShingle | Electrical Engineering and Computer Science. Near, Joseph P. (Joseph Paul) An imperative extension to alloy and a compiler for its execution |
| title | An imperative extension to alloy and a compiler for its execution |
| title_full | An imperative extension to alloy and a compiler for its execution |
| title_fullStr | An imperative extension to alloy and a compiler for its execution |
| title_full_unstemmed | An imperative extension to alloy and a compiler for its execution |
| title_short | An imperative extension to alloy and a compiler for its execution |
| title_sort | imperative extension to alloy and a compiler for its execution |
| topic | Electrical Engineering and Computer Science. |
| url | http://hdl.handle.net/1721.1/60178 |
| work_keys_str_mv | AT nearjosephpjosephpaul animperativeextensiontoalloyandacompilerforitsexecution AT nearjosephpjosephpaul imperativeextensiontoalloyandacompilerforitsexecution |