Type Systems and Static Analyses for Programs with Mutable Data

具有可变数据的程序的类型系统和静态分析

• 批准号: RGPIN-2020-04021
• 负责人: Lhotak, Ondrej
• 金额: $ 3.5万
• 依托单位: University of Waterloo
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2021
• 资助国家: 加拿大
• 起止时间: 2021-01-01 至 2022-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=739628
• 关键词: Type; Systems; Static; Analyses; Programs

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.

人们编写程序来使计算机执行某些操作或计算某些结果。程序指定要执行的步骤。预测这些步骤的结果，即程序在运行时的行为，是重要的，但往往是困难的。当一个程序的行为与预期的不同时，它会造成软件故障，可能导致巨大的金钱损失甚至身体伤害。本研究的目标是以两种互补的方式加强程序与其行为之间的对应关系：首先，通过增强编程语言来表达不仅要执行的步骤，而且要表达预期的结果，精确到计算机可以验证这些步骤是否实现了结果;第二，通过改进预测可能的程序行为的技术，以利用指定的预期结果进行更精确的推理。其结果将是程序员更好地传达他们的意图，以及更好的工具来检查程序是否实现了意图。现有的研究已经产生了强大的技术来描述纯粹功能性程序的行为，因为它们从不覆盖现有数据，只生成新数据。但许多真实的程序确实会修改现有数据，因此最常用的编程语言都是围绕数据更新设计的。我将致力于混合语言，在可能的情况下启用函数式风格，但在需要时允许更新。我将从纯函数式语言中借鉴一些强大的技术，但我必须扩展它们，以便在数据更新发生时仍能工作。拟议的研究将使目前仅适用于研究语言的技术可用于编写大多数真实的程序的流行编程语言。这项研究将影响人们如何思考和交流计算机程序如何更新数据。其影响超出了向计算机传达意图。编写程序的人在心理上理解这些程序应该如何工作。通过提供一种以书面形式记录这种理解的语言，这项研究将使人们能够更准确地相互交流这种理解。通过使这种理解明确和精确，所提出的研究也将帮助程序员更清楚地思考程序，更容易注意到概念错误。最终的影响将是更可靠的软件。本研究涉及理论和实践两个方面。在理论方面，我们必须确保程序行为的描述具有精确和明确的含义，并且验证技术本身是正确的。在实践方面，我们必须实现编程工具的变化，并研究它们如何适用于现有程序。我将在这两方面培养研究生。他们将成为编程语言和编程工具的专家，能够领导世界一流的研究和生产新的软件开发工具。