Proving Theorems About Java-Like Byte Code
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.
KeywordsSemantic Function Program Counter Java Virtual Machine Computational Logic Instance Method
Unable to display preview. Download preview PDF.
- 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
- 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.R. S. Boyer and J S. Moore. A Computational Logic Handbook, Second Edition, Academic Press: London, 1997.Google Scholar
- 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.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://firstname.lastname@example.org).
- 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
- 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.T. Lindholm and F. Yellin The Java Virtual Machine Specification, Addison-Wesley, 1996.Google Scholar
- 11.J S. Moore. Piton: A Mechanically Verified Assembly-Level Language. Automated Reasoning Series, Kluwer Academic Publishers, 1996.Google Scholar
- 13.W. D. Young, A Verified Code-Generator for a Subset of Gypsy, PhD Thesis, University of Texas at Austin” 1988.Google Scholar
- 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