Executable specifications for Java programs
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
2011
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/1721.1/62442 |
| _version_ | 1826207039542525952 |
|---|---|
| author | Milicevic, Aleksandar, Ph. D. Massachusetts Institute of Technology |
| author2 | Daniel N. Jackson. |
| author_facet | Daniel N. Jackson. Milicevic, Aleksandar, Ph. D. Massachusetts Institute of Technology |
| author_sort | Milicevic, Aleksandar, Ph. D. Massachusetts Institute of Technology |
| collection | MIT |
| description | Thesis (S.M.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2010. |
| first_indexed | 2024-09-23T13:42:32Z |
| format | Thesis |
| id | mit-1721.1/62442 |
| institution | Massachusetts Institute of Technology |
| language | eng |
| last_indexed | 2024-09-23T13:42:32Z |
| publishDate | 2011 |
| publisher | Massachusetts Institute of Technology |
| record_format | dspace |
| spelling | mit-1721.1/624422019-04-12T16:10:34Z Executable specifications for Java programs Milicevic, Aleksandar, Ph. D. Massachusetts Institute of Technology Daniel N. 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. Cataloged from PDF version of thesis. Includes bibliographical references (p. 55-57). In this thesis, we present a unified environment for running declarative specifications in the context of an imperative object-oriented programming language. Specifications are Alloy-like, written in first-order relational logic with transitive closure, and the imperative language for this purpose is Java. By being able to mix imperative code with executable declarative specifications, the user can easily express constraint problems in-place, i.e. in terms of the existing data structures and objects on the heap. After a solution is found, our framework will automatically update the heap to reflect the solution, so the user can continue to manipulate the program heap in the usual imperative way, without ever having to manually translate the problem back and forth between the host programming environment and the solver language. We show that this approach is not only convenient, but, for certain problems, like puzzles or NP-complete graph algorithms, it can also outperform the manual implementation. We also present an optimization technique that allowed us to run our tool on heaps with almost 2000 objects. by Aleksandar Milicevic. S.M. 2011-04-25T15:59:24Z 2011-04-25T15:59:24Z 2010 2010 Thesis http://hdl.handle.net/1721.1/62442 711072554 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 57 p. application/pdf Massachusetts Institute of Technology |
| spellingShingle | Electrical Engineering and Computer Science. Milicevic, Aleksandar, Ph. D. Massachusetts Institute of Technology Executable specifications for Java programs |
| title | Executable specifications for Java programs |
| title_full | Executable specifications for Java programs |
| title_fullStr | Executable specifications for Java programs |
| title_full_unstemmed | Executable specifications for Java programs |
| title_short | Executable specifications for Java programs |
| title_sort | executable specifications for java programs |
| topic | Electrical Engineering and Computer Science. |
| url | http://hdl.handle.net/1721.1/62442 |
| work_keys_str_mv | AT milicevicaleksandarphdmassachusettsinstituteoftechnology executablespecificationsforjavaprograms |