A CONTEXT AWARE TYPE SYSTEM FOR TREE-LIKE DATA STRUCTURES

Abstract

In this work, we design a context aware type system for an imperative programming language where all data are tree structures. Tree-like data structures can have different forms with distinct fields based on the way they are constructed. Our type system can determine the forms of data trees from a program context and ensure the correctness of field accesses and function applications. During type checking, the program context is approximated as a function that maps each program point to a set of possible program states. Indexing information is also approximated with special array range states and relative order of indices. This novel treatment of indices allows us to reason about the state of an array at some index without storing the states of individual elements. Once the program approximation is computed, the type-checking algorithm ensures the correctness of function and field applications. Function and field applications are valid if their preconditions are satisfied by the current program state. A program is well-typed if all function applications and field accesses can be resolved to exactly one valid overload in each possible program state. Otherwise, our type-checking algorithm concludes that the program is ill-typed.