Abstract
This paper presents an extension of the standard bitvector library of the theorem prover PVS with multiplication, division and remainder operations, together with associated results. This extension is needed to give correct semantics to Java’s integral types in program verification. Special emphasis is put on Java’s widening and narrowing functions in relation to the newly defined operations on bitvectors.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Ahrendt, W., Baar, T., Beckert, B., Giese, M., Hähnle, R., Menzel, W., Mostowski, W., Schmitt, P.H.: The KeY system: Integrating object-oriented design and formal methods. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, pp. 327–330. Springer, Heidelberg (2002)
Beckert, B., Schlager, S.: Integer arithmetic in the specification and verification of Java programs. In: Workshop on Tools for System Design and Verification, FM-TOOLS (2002), http://i12www.ira.uka.de/~beckert/misc.html
van den Berg, J., Jacobs, B.: The LOOP compiler for Java and JML. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 299–312. Springer, Heidelberg (2001)
Carreño, V.A., Miner, P.S.: Specification of the IEEE-854 floating-point standard in HOL and PVS. In: Schubert, E.T., Windley, P.J., Alves-Foss, J. (eds.) Higher Order Logic Theorem Proving and Its Applications. Category B Proceedings (1995)
Chalin, P.: Improving jml: For a safer and more effective language. In: Formal Methods Europe 2003 (2003) (to appear)
Chen, Z.: Java Card Technology for Smart Cards. The Java Series. Addison-Wesley, Reading (2000)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). SIGPLAN Notices, vol. 37(5), pp. 234–245. ACM, New York (2002)
Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification, 2nd edn. The Java Series. Addison-Wesley, Reading (2000)
Harrison, J.: A machine-checked theory of floating point arithmetic. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 113–130. Springer, Heidelberg (1999)
Harrison, J.: Formal verification of IA-64 division algorithms. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 234–251. Springer, Heidelberg (2000)
Jacobs, B., Oostdijk, M., Warnier, M.: Formal verification of a secure payment applet. Journ. of Logic and Algebraic Programming (to appear)
Leavens, G.T., Baker, A.L., Ruby, C.: JML: A notation for detailed design. In: Kilov, H., Rumpe, B. (eds.) Behavioral Specifications of Business and Systems, pp. 175–188. Kluwer, Dordrecht (1999)
Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C.: JML reference manual, draft (2003), http://www.jmlspecs.org
Marché, C., Paulin, C., Urbain, X.: The Krakatoa tool for certification java/javacard programs annotated in jml. Journ. of Logic and Algebraic Programming (to appear)
Owre, S., Rushby, J.M., Shankar, N., von Henke, F.: Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Trans. on Softw. Eng. 21(2), 107–125 (1995)
Rauch, N., Wolff, B.: Formalizing Java’s two’s-complement integral type in Isabelle/HOL. In: Arts, T., Fokkink, W. (eds.) Formal Methods for Industrial Critical Systems (FMICS 2003). Elect. Notes in Theor. Comp. Sci, vol. 80. Elsevier, Amsterdam (2003), www.elsevier.nl/locate/entcs/volume80.html
Stallings, W.: Computer Organization and Architecture, 4th edn. Prentice Hall, Englewood Cliffs (1996)
Théry, L.: A library for floating-point numbers in Coq (2002), http://www-sop.inria.fr/lemme/AOC/coq/
Winkler, J.F.H.: A safe variant of the unsafe integer arithmetic of Java TM. Software – Practice and Experience 33, 669–701 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 IFIP International Federation for Information Processing
About this paper
Cite this paper
Jacobs, B. (2003). Java’s Integral Types in PVS. In: Najm, E., Nestmann, U., Stevens, P. (eds) Formal Methods for Open Object-Based Distributed Systems. FMOODS 2003. Lecture Notes in Computer Science, vol 2884. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39958-2_1
Download citation
DOI: https://doi.org/10.1007/978-3-540-39958-2_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20491-6
Online ISBN: 978-3-540-39958-2
eBook Packages: Springer Book Archive