ACL2 in DrScheme

ABSTRACT

Teaching undergraduates to develop software in a formal framework such as ACL2 poses two immediate challenges. First, students typically do not know applicative programming and are often unfamiliar with ACL2's syntax. Second, for motivational reasons, students prefer to work on projects that involve designing interactive, graphical applications.In this paper, we present DRACULA, a pedagogic programming environment that partially solves these problems. The environment adds a subset of Applicative Common Lisp to DRSCHEME, an integrated programming environment for Scheme. DRACULA thus inherits DRSCHEME's pedagogic capabilities, especially its treatment of syntax and run-time errors. Further, DRACULA also comes with a library for programming interactive, graphical games. The library interface forces students to think of a graphical user interface in terms of state-transition functions, enabling them later to prove theorems about their games in ACL2. DRACULA provides a graphical front-end to the ACL2 theorem prover for this purpose. In short, DRACULA allows the formulation of student projects that represent an important intermediate point between data structure exercises in theorem proving and industrial applications.

REFERENCES

• 1: David Aspinall, Proof General: A Generic Tool for Proof Development, Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems: Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, p.38-42, March 25-April 02, 2000
• 2: Robert S. Boyer , J. Strother Moore, Mechanized formal reasoning about programs and computing machines, Automated reasoning and its applications: essays in honor of Larry Wos, MIT Press, Cambridge, MA, 1997
• 3: Dillinger, P., P. Manolios and D. Vroon. ACL2s: The ACL2 Sedan. http://naxos.cc.gt.atl.ga.us/acl2s/, 2006.
• 4: Eclipse Consortium. Eclipse, 2000. http://www.eclipse.org.
• 5: M. Felleisen , R. B. Findler , M. Flatt , S. Krishnamurthi, The DrScheme project: an overview, ACM SIGPLAN Notices, v.33 n.6, p.17-23, June 1998 [doi>10.1145/284563.284566]
• 6: Felleisen, M., R. B. Findler, M. Flatt and S. Krishnamurthi. How to Design Programs. MIT Press, 2001.
• 7: Felleisen, M., R. B. Findler, M. Flatt and S. Krishnamurthi. The TeachScheme! project: Computing and programming for every student. Computer Science Education, 14:55--77, 2004.
• 8: Findler, R. B. PLT DrScheme: Programming environment manual. Technical Report PLT-TR05-3-v300, PLT Scheme Inc., 2005. http://www.plt-scheme.org/techreports/.
• 9: Robert Bruce Findler , John Clements , Cormac Flanagan , Matthew Flatt , Shriram Krishnamurthi , Paul Steckler , Matthias Felleisen, DrScheme: a programming environment for Scheme, Journal of Functional Programming, v.12 n.2, p.159-182, March 2002 [doi>10.1017/S0956796801004208]
• 10: Robert Bruce Findler , Matthias Felleisen, Contracts for higher-order functions, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.48-59, October 04-06, 2002, Pittsburgh, PA, USA
• 11: Matthew Flatt, Composable and compilable macros:: you want it when?, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.72-83, October 04-06, 2002, Pittsburgh, PA, USA
• 12: Flatt, M. PLT MzScheme: Language manual. Technical Report PLT-TR05-1-v300, PLT Scheme Inc., 2005. http://www.plt-scheme.org/techreports/jfp01-fcffksf.
• 13: Flatt, M. and R. B. Findler. PLT MrEd: Graphical toolbox manual. Technical Report PLT-TR05-2-v300, PLT Scheme Inc., 2005. http://www.plt-scheme.org/techreports/.
• 14: Harper, R. and B. C. Pierce. Design issues in advanced module systems. In Pierce, B. C., editor, Advanced Topics in Types and Programming Languages. MIT Press, 2004.
• 15: Kaufmann, M., P. Manolios and J. S. Moore. Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers, 2000.
• 16: Rex Page, Engineering software correctness, Proceedings of the 2005 workshop on Functional and declarative programming in education, September 25-25, 2005, Tallinn, Estonia [doi>10.1145/1085114.1085123]
• 17: Peyton-Jones, S., editor. Haskell 98 Language and Libraries The Revised Report. Cambridge University Press, Cambridge, UK, April 2003.
• 18: Plotkin, G. D. Call-by-name, call-by-value, and the λ-calculus. Theoretical Computer Science, pages 125--159, 1975.
• 19: The Coq Development Team. The Coq Proof Assistant Reference Manual. LogiCal Project, INRIA, 8.0 edition. http://coq.inria.fr/doc/main.html.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.6 Programming Environments

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

  K. Computing Milieux
  K.3 COMPUTERS AND EDUCATION
      K.3.2 Computer and Information Science Education

Keywords:
ACL2, DrScheme, TeachScheme!, formal methods, pedagogy