Advertisement

Proving Theorems About Java-Like Byte Code

  • J Strother Moore
Chapter
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1710)

Abstract

We describe a formalization of an abstract machine very similar to the Java Virtual Machine but far simpler. We develop techniques for specifying the properties of classes and methods for this machine. We develop techniques for mechanically proving theorems about classes and methods.We discuss two such proofs, that of a static method implementing the factorial function and of an instance method that destructively manipulates objects in a way that takes advantage of inheritance. We conclude with a brief discussion of the advantages and disadvantages of this approach. The formalization and proofs are done with the ACL2 theorem proving system.

Keywords

Semantic Function Program Counter Java Virtual Machine Computational Logic Instance Method 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    W. R. Bevier, W. A. Hunt, J S. Moore, and W. D. Young. Special Issue on System Verification. Journal of Automated Reasoning, 5(4):409–530, December, 1989.Google Scholar
  2. 2.
    R. S. Boyer and J S. Moore. A Computational Logic. Academic Press: New York, 1979.zbMATHGoogle Scholar
  3. 3.
    R. S. Boyer and J S. Moore. Mechanized Formal Reasoning about Programs and Computing Machines. In R. Veroff (ed.), Automated Reasoning and Its Applications: Essays in Honor of Larry Wos, MIT Press, 1996.Google Scholar
  4. 4.
    R. S. Boyer and J S. Moore. A Computational Logic Handbook, Second Edition, Academic Press: London, 1997.Google Scholar
  5. 5.
    B. Brock, M. Kaufmann and J S. Moore, “ACL2 Theorems about Commercial Microprocessors,” in M. Srivas and A. Camilleri (eds.) Proceedings of Formal Methods in Computer-Aided Design (FMCAD‘96), Springer-Verlag, pp. 275–293, 1996.Google Scholar
  6. 6.
    R. M. Cohen, The Defensive Java Virtual Machine Specification, Version 0.53, Electronic Data Systems, Corp, Austin Technical Services Center, 98 San Jacinto Blvd, Suite 500, Austin, TX 78701 email:(http://cohen@aus.edsr.eds.com).
  7. 7.
    A. D. Flatau, A verified implementation of an applicative language with dynamic storage allocation, PhD Thesis, University of Texas at Austin, 1992.Google Scholar
  8. 8.
    M. Kaufmann and J Strother Moore “An Industrial Strength Theorem Prover for a Logic Based on Common Lisp,”IEEE Transactions on Software Engineering, 23(4), pp. 203–213, April, 1997CrossRefGoogle Scholar
  9. 9.
    M. Kaufmann and J Strother Moore “A Precise Description of the ACL2 Logic,” http://www.cs.utexas.edu/users/moore/publications/-km97a.ps.Z, April, 1998.
  10. 10.
    T. Lindholm and F. Yellin The Java Virtual Machine Specification, Addison-Wesley, 1996.Google Scholar
  11. 11.
    J S. Moore. Piton: A Mechanically Verified Assembly-Level Language. Automated Reasoning Series, Kluwer Academic Publishers, 1996.Google Scholar
  12. 12.
    G. L. Steele, Jr. Common Lisp The Language, Second Edition. Digital Press, 30 North Avenue, Burlington, MA 01803, 1990.zbMATHGoogle Scholar
  13. 13.
    W. D. Young, A Verified Code-Generator for a Subset of Gypsy, PhD Thesis, University of Texas at Austin” 1988.Google Scholar
  14. 14.
    Y. Yu. Automated Proofs of Object Code For a Widely Used Microprocessor. PhD thesis, University of Texas at Austin, 1992. Lecture Notes in Computer Science, Springer-Verlag (to appear). ftp://ftp.cs.utexas.edu/pub-/techreports/tr93-09.ps.Z

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • J Strother Moore
    • 1
  1. 1.Department of Computer SciencesUniversity of Texas at AustinUSA

Personalised recommendations