Mitigating human error in programs through combined language/reasoning systems

通过组合语言/推理系统减少程序中的人为错误

• 批准号: 0541447
• 负责人: Tim Sheard
• 金额: $ 30万
• 依托单位: Portland State University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2006
• 资助国家: 美国
• 起止时间: 2006-04-01 至 2010-03-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0541447&HistoricalAwards=false
• 关键词: Mitigating; human; error; programs; through

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.

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