SHF: Small: Collaborative Research: Modular 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.