Mitigating human error in programs through combined language/reasoning systems

获奖摘要0541447 tim sheard波特兰州立大学通过组合语言/推理系统减少程序中的人为错误。研究了组合编程/推理工具的理论和实践。该策略是使程序员能够定义和推理他们的程序，根据他们自己定义的属性进行转换，所有这些都来自编程语言本身。开发的系统将使用增强的类型系统直接对程序（而不是模型）进行推理，以获取程序员直接感兴趣的属性。该项目将开发一个组合编程/推理系统的可靠理论，并通过扩展和改进现有的Omega语言来应用该理论。该系统将具有四个重要特征，使其区别于其他竞争方法。(1)程序员定义的每个属性在编程语言中具有独立于其作为逻辑实体的角色的语义含义。(2)系统将值与类型分开，以保持熟悉的编程风格。(3)约束的管理在语言内部执行，使用易于理解的约束类型机制。(4)系统将约束管理分为静态和动态两部分，允许用户选择在编译时或运行时何时解除约束。结合编程/推理工具的更广泛的影响是使程序员能够构建更高质量的软件。推理能力允许有效的分工：专家通过指定其属性来设计软件，而有能力的程序员填充细节。推理工具检查构造的软件实际上包含所需的属性。

Award Abstract0541447Tim SheardPortland State UniversityMitigating Human Error in Programs Through Combined Language/Reasoning Systems.The theory and practice of combined programming/reasoning tools is investigated. The strategy is to enable programmers to define and reason about their programs, cast in terms of properties they defined themselves, all from within the programming language itself. The system developed will reason directly about programs (not models) using enhanced type systems to capture the properties of direct interest to the programmer. The project will develop a sound theory of combined programming/reasoning systems, and apply that theory by extending and refining the existing Omega language.The system will have four important characteristics that separate it from competing approaches. (1) Each property defined by the programmer has semantic meaning within the programming language independent of its role as a logical entity. (2) The systems separates values from types to maintain a familiar programming style. (3) Management of the constraints is performed inside the language using the well understood mechanism of constrained types. And, (4) The system partitions constraint management into static and dynamic parts, allowing the user to choose when constraints can be discharged at compile-time or at run-time.The broader impacts of combined programming/reasoning tools is to enable programmers to construct higher quality software. The reasoning capabilities allow an efficient division of labor:Experts design software by specifying its properties, and competent programmers fill in the details. The reasoning facilities check that the constructed software actually contains the desired properties.