SHF: SMALL: Collaborative Research: Modular ACL2

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

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.