Type Systems and Static Analyses for Programs with Mutable Data

点击翻译按钮获取中文摘要

People write programs to cause a computer to perform some action or compute some result. The program specifies the steps to be executed. Predicting the outcome of those steps, how the program will behave when it runs, is important but often difficult. When a program behaves differently than intended, it creates a software failure that can cause huge monetary losses or even physical harm. The goal of this research is to strengthen the correspondence between programs and their behaviour in two complementary ways: first, by enhancing programming languages to express not only the steps to be executed, but also the intended outcomes, precisely enough that a computer can verify that the steps achieve the outcomes; second, by improving techniques for predicting possible program behaviours to take advantage of the specified intended outcomes for more precise reasoning. The result will be better ways for programmers to communicate their intent and better tools for checking that programs achieve that intent. Existing research has produced powerful techniques for describing the behaviour of programs that are purely functional, in that they never overwrite existing data and only generate new data. But many real programs do modify existing data, so the most commonly used programming languages are designed around data updates. I will work on hybrid languages that enable a functional style when possible, but allow updates when needed. I will draw on some powerful techniques from purely functional languages, but I will have to extend them to still work when data updates do occur. The proposed research will make techniques that currently only apply to research languages available for the popular programming languages used to write most real programs. This research will impact how people think and communicate about how computer programs update data. The impact goes beyond communicating intent to the computer. People who write programs have a mental understanding of how those programs should work. By providing a language to record that understanding in written form, this research will enable people to more precisely communicate this understanding to each other. By making this understanding explicit and precise, the proposed research will also help programmers think more clearly about the program and more easily notice conceptual errors. The final impact will be more reliable software. The proposed research involves both theory and practice. On the theoretical side, we must ensure that the descriptions of program behaviour have precise and unambiguous meanings and that the verification techniques are themselves correct. On the practical side, we must implement the changes in programming tools and study how well they apply to existing programs. I will train graduate students in both aspects. They will become experts in programming languages and programming tools, capable of leading world-class research and producing new software development tools.