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.
Engineers use calculus and analysis to model and understand new productssuch as airplanes, bridges, machines, oil drilling techniques, roads, andskyscrapers. Similarly, software engineering rests on logic, a relativelynew, foundational field of mathematics. Unfortunately, many computerscience departments teach logic in courses that is disjoint from the restof the curriculum. In particular, it does not relate logic to the majoractivities of working software engineers: collecting requirements,articulating specifications, designing programs, and relating programs totheir specifications. This projected aimed to address this gap between teaching of logic and thereality of engineering software. While Prof. Rex Page at Oklahoma focusedon the development of teaching materials, the team at Northeasternconstructed an integrated development environment (IDE) for stating logicaltheorems about programs, designing programs, and proving the theorems aboutthe programs. In addition, the team designed and implemented a modularversion of ACL2 so that Page's course on software engineering couldintroduce the idea of modular reasoning about software. DrACuLa, the IDE, extends DrRacket and integrates it with the ACL2 theoremprover. The Northeastern team developed the IDE and tested it in asecond-semester freshman course. It held up well for four years of Page'ssoftware engineering course. Over this time, the Northeastern team regularly consulted with Page at Oklahoma to fix flaws in the IDE and to add the desired functionality. See the attached screenshot; it shows a small graphical interactive (GUI) program that a freshman student might design. The screen shot shows how the student learn to articulate basic claims about the various GUI event-handling functions in the program.One way to articulate such a claim is to formulate a randomly checked property. Once the random property checker cannot find counter-examples, the student would reformulate the property as a logical theorems and ask DrACuLa to prove the theorem. The IDE performs this task by calling out to the ACL2 theorem prover, which is also used by various hardware companies to verify the workings of computers. For the second goal, the Northeastern team designed and implemented threedifferent module systems for ACL2, dubbed Modular ACL2. The team evaluatedeach design with respect to its expressiveness and usefulness, usually onrealistic large, multi-module software systems. Over the course of theinvestigation, it became clear that even though the module systemssupported Page's teaching project, they failed to advance ACL2'scapabilities. The team identified ACL2's old-fashioned macro system as thekey problem. Unfortunately, attempts to add a modern macro system toModular ACL2 into the theorem prover were unsuccessful due to seriousperformance problems. Resources permitting the team will continue tomaintain the software and to continue the search for a performantsolution. In sum, the project showed the feasibility of integrating programming and logic for students as early as the freshman year. Northeastern continues to teach this course (with a different flavor of ACL2) and CMU faculty have stated their desire to catch up with this novel curriculum. Page has demonstrated that software engineering capstone courses can benefit from the integration of logic and program design.
