Type flow analysis for exploratory software development

Exploratory programming languages and development enjoy a reputation for enabling both rapid development of prototype implementations and ease of evolution as experience with these prototypes suggests improvements. However, the exploratory paradigm also suffers from a reputation for producing brittle systems, prone to errors and run-time failure. The run-time, dynamic typing associated with exploratory languages contributes to both of these reputations. On the one hand, the ability of exploratory programs to define new types during execution and to dispatch based upon the types of data objects facilitates development by providing powerful forms of polymorphism and abstraction. On the other hand, these same capabilities preclude conventional approaches to compile-time assessment of type safety, such as the declaration-based mechanisms in languages like Pascal, or the inference mechanisms in functional languages like ML. This dissertation describes a program analysis technique called type flow analysis that assesses the type safety of programs written in Lisp. Type flow analysis differs from other compile-time assessment approaches in mechanism and in application. Its mechanism comprises a novel synthesis of polymorphic type inference, symbolic execution, and declaration-based approaches. It is applied as part of an incremental, evolutionary approach to the development of verifiably type safe exploratory programs. Type flow analysis improves the exploratory paradigm by enabling a system to smoothly evolve from an initial, weakly typed prototype to a more robust, strongly typed end product