SHF: Small: Collaborative Research: Modular ACL2

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

Reliability is extremely important for some software and hardwareapplications. One approach is to use a programming language with amechanized logic---a so-called theorem-prover---to prove theorems thatestablish some critical behavioral characteristics. Among theorem-provers,ACL2 has found use with several industrial suppliers of high assurancesoftware and hardware. ACL2 does not support component-oriented softwaredevelopment, however, making it difficult to use with large and complexprojects.This research project has three goals: to add a pragmatic module system toACL2; to equip it with a hygienic macro system; and to investigate a typesystem that accommodates ACL2's programming idioms. The project teamemploys a cyclic, three-step exploration method. The first step is toadapt constructs from existing, similar languages to ACL2, especially alogical meaning consistent with the theorem prover of ACL2. The secondstep is to explore the pragmatics of the design with a wide range ofexamples. The third step is to add implementations to a pedagogic,interactive development environment for ACL2 and to evaluate theirusefulness in software engineering courses. The results of this last stepare used to re-start the cycle.The work will contribute to the dissemination of theorem provers inclassrooms and industry. The research team expects to expose collegestudents to the use of theorem proving in the design and development ofcomplex systems with dozens, and possibly hundreds, of reliablecomponents. The team also hopes to improve the ability of industrial ACL2programmers to tackle complex component-oriented systems.