SafeJava: A Unified Type System for Safe Programming Export

@misc{citeulike:5800902, abstract = {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}, author = {Boyapati, Chandrasekhar and Boyapati, Chandrasekhar and Rinard, Martin C.}, citeulike-article-id = {5800902}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.144.5905}, keywords = {compilers, concurrency, java, programming-language-design, type-theory}, posted-at = {2009-09-18 03:06:42}, priority = {2}, title = {SafeJava: A Unified Type System for Safe Programming}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.144.5905}, year = {2004} }

TY - ELEC ID - citeulike:5800902 L3 - citeulike-article-id:5800902 N2 - 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 TI - SafeJava: A Unified Type System for Safe Programming KW - compilers KW - concurrency KW - java KW - programming-language-design KW - type-theory AU - Boyapati, Chandrasekhar AU - Boyapati, Chandrasekhar AU - Rinard, Martin PY - 2004/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.144.5905 ER -