SHF: SMALL: Collaborative Research: Modular ACL2

SHF：小型：协作研究：模块化 ACL2

• 批准号: 1016532
• 负责人: Rex Page
• 金额: $ 20万
• 依托单位: University of Oklahoma Norman Campus
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2010
• 资助国家: 美国
• 起止时间: 2010-08-15 至 2013-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1016532&HistoricalAwards=false
• 关键词: SHF; SMALL; Collaborative; Research; Modular

Reliability is extremely important for some software and hardware applications. One approach is to use a programming language with a mechanized logic---a so-called theorem-prover---to prove theorems that establish some critical behavioral characteristics. Among theorem-provers, ACL2 has found use with several industrial suppliers of high assurance software and hardware. ACL2 does not support component-oriented software development, however, making it difficult to use with large and complex projects. This research project has three goals: to add a pragmatic module system to ACL2; to equip it with a hygienic macro system; and to investigate a type system that accommodates ACL2's programming idioms. The project team employs a cyclic, three-step exploration method. The first step is to adapt constructs from existing, similar languages to ACL2, especially a logical meaning consistent with the theorem prover of ACL2. The second step is to explore the pragmatics of the design with a wide range of examples. The third step is to add implementations to a pedagogic, interactive development environment for ACL2 and to evaluate their usefulness in software engineering courses. The results of this last step are used to re-start the cycle. The work will contribute to the dissemination of theorem provers in classrooms and industry. The research team expects to expose college students to the use of theorem proving in the design and development of complex systems with dozens, and possibly hundreds, of reliable components. The team also hopes to improve the ability of industrial ACL2 programmers to tackle complex component-oriented systems.

可靠性对于一些软件和硬件应用来说是极其重要的。一种方法是使用一种带有机械化逻辑的编程语言——一种所谓的定理证明器——来证明建立一些关键行为特征的定理。在定理证明者中，ACL2已经被一些高保证软件和硬件的工业供应商所使用。然而，ACL2不支持面向组件的软件开发，这使得它很难用于大型和复杂的项目。本研究项目有三个目标：为ACL2添加一个语用模块系统；配备卫生宏观系统；并研究一种适应ACL2编程习惯的类型系统。项目团队采用循环的三步勘探方法。第一步是将现有的类似语言的结构改编为ACL2，特别是与ACL2的定理证明一致的逻辑含义。第二步是通过广泛的实例来探索设计的语用学。第三步是为ACL2的教学、交互开发环境添加实现，并评估它们在软件工程课程中的有用性。最后一步的结果用于重新启动循环。这项工作将有助于定理证明者在课堂和行业的传播。研究小组希望让大学生们在设计和开发包含数十个，甚至数百个可靠组件的复杂系统时，接触到定理证明的应用。该团队还希望提高工业ACL2程序员处理复杂面向组件系统的能力。