SafeJava : a unified type system for safe programming
Thesis (Ph. D.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, February 2004.
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | eng |
| Published: |
Massachusetts Institute of Technology
2006
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/1721.1/30087 |
| _version_ | 1811085901184368640 |
|---|---|
| author | Boyapati, Chandrasekhar, 1973- |
| author2 | Martin C. Rinard. |
| author_facet | Martin C. Rinard. Boyapati, Chandrasekhar, 1973- |
| author_sort | Boyapati, Chandrasekhar, 1973- |
| collection | MIT |
| description | Thesis (Ph. D.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, February 2004. |
| first_indexed | 2024-09-23T13:17:18Z |
| format | Thesis |
| id | mit-1721.1/30087 |
| institution | Massachusetts Institute of Technology |
| language | eng |
| last_indexed | 2024-09-23T13:17:18Z |
| publishDate | 2006 |
| publisher | Massachusetts Institute of Technology |
| record_format | dspace |
| spelling | mit-1721.1/300872019-04-10T21:34:00Z SafeJava : a unified type system for safe programming Unified type system for safe programming Boyapati, Chandrasekhar, 1973- Martin C. Rinard. 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 (Ph. D.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, February 2004. Includes bibliographical references (p. 155-164). Making software reliable is one of the most important technological challenges facing our society today. This thesis presents a new type system that addresses this problem by statically preventing several important classes of programming errors. If a program type checks, we guarantee at compile time that the program does not contain any of those errors. We designed our type system in the context of a Java-like object-oriented language; we call the resulting system SafeJava. The SafeJava type system offers significant software engineering benefits. Specifically, it provides a statically enforceable way of specifying object encapsulation and enables local reasoning about program correctness; it combines effects clauses with encapsulation to enable modular checking of methods in the presence of subtyping; it statically prevents data races and deadlocks in multithreaded programs, which are known to be some of the most difficult programming errors to detect, reproduce, and eliminate; it enables software upgrades in persistent object stores to be defined modularly and implemented efficiently; it statically ensures memory safety in programs that manage their own memory using regions; and it also statically ensures that real-time threads in real-time programs are not interrupted for unbounded amounts of time because of garbage collection pauses. Moreover, SafeJava provides all the above benefits in a common unified type system framework, indicating that seemingly different problems such as encapsulation, synchronization issues, software upgrades, and memory management have much in common. (cont.) We have implemented several Java programs in SafeJava. Our experience shows that SafeJava is expressive enough to support common programming patterns, its type checking is fast and scalable, and it requires little programming overhead. In addition, the type declarations in SafeJava programs serve as documentation that lives with the code, and is checked throughout the evolution of code. The SafeJava type system thus has significant software engineering benefits and it offers a promising approach for improving software reliability. by Chandrasekhar Boyapati. Ph.D. 2006-03-24T18:18:16Z 2006-03-24T18:18:16Z 2003 2004 Thesis http://hdl.handle.net/1721.1/30087 55667518 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 164 p. 8038595 bytes 8038403 bytes application/pdf application/pdf application/pdf Massachusetts Institute of Technology |
| spellingShingle | Electrical Engineering and Computer Science. Boyapati, Chandrasekhar, 1973- SafeJava : a unified type system for safe programming |
| title | SafeJava : a unified type system for safe programming |
| title_full | SafeJava : a unified type system for safe programming |
| title_fullStr | SafeJava : a unified type system for safe programming |
| title_full_unstemmed | SafeJava : a unified type system for safe programming |
| title_short | SafeJava : a unified type system for safe programming |
| title_sort | safejava a unified type system for safe programming |
| topic | Electrical Engineering and Computer Science. |
| url | http://hdl.handle.net/1721.1/30087 |
| work_keys_str_mv | AT boyapatichandrasekhar1973 safejavaaunifiedtypesystemforsafeprogramming AT boyapatichandrasekhar1973 unifiedtypesystemforsafeprogramming |