SHF: SMALL: Collaborative Research: Modular ACL2

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

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.