ITR: Static Checking in an Extended Type System

Sri International, Menlo Park CA

Investigators

Abstract

CCR-0082560 Static Checking in an Extended Type System PIs: Natarajan Shankar and Sam Owre Abstract: A safe programming language is one whose type system can, at compile time, detect potential runtime errors such as null dereferences, out-of-bounds array indices, division by zero, and inapplicable method invocations. Few widely used programming languages are safe in this sense. Specification languages like PVS, however, contain safety features such as predicate subtypes and dependent types that can be used to ensure the absence of runtime errors. The design of safe programming languages requires an integration of specification and programming languages through the use of enriched type systems. These types increase the expressiveness and naturalness of both executable descriptions (programs) and non-executable descriptions (mathematical specifications). We extend the type systems for widely used languages, such as Java, with PVS-like specification constructs. We develop an effective static typechecker for this type system that detects many common programming errors. The research builds on advances in programming languages, type theories, program optimization techniques, decision procedures, and program analysis methods, and tools such as LCLint, ESC, and BANE. An extended type system for programming languages can be a foundation for the design and development of well-specified, efficient, and safe programs.