Skip to content

Quicktour

Abstract

This article gives an introduction to the KeY system.

Introduction

When we started writing this document, we aimed at providing a short tutorial accompanying the reader at their first steps with the KeY system. The KeY tool is designed as an integrated environment for creating, analyzing, and verifying software models and their implementation. The reader shall learn how to install and use the basic functionality of the KeY tool. Besides practical advises how to install and get KeY started, we show along a small project how to use the KeY tool to verify programs.

Verification means proving that a program complies with its specification in a mathematically rigorous way. In order to fulfill this task, the specification needs to be given in a formal language with a precisely defined meaning. In the current version of the document, we focus on the popular Java Modeling Language (JML) 1415 as specification language.

In the next sections, we show how to verify a JML-annotated (specified) JavaCard program. For this purpose, KeY features a calculus for the complete JavaCard language including advanced features like transactions.

Besides JML, the KeY tool supports JavaCardDL as a specification language.

For a longer discussion on the architecture, design philosophy, and theoretical underpinnings of the KeY tool  please refer to 1. In case of questions or comments, don't hesitate to contact the KeYsupport team at (mailto:support@key-project.org).

Version Information

This tutorial was tested for KeY version 2.10.

Contents

  1. Installation: This chapter explains how to install and run the KeY system.
  2. Loading JML Contracts: This chapter explains how to load JML specifications into KeY and gives an introduction to the logical calculus behind KeY.
  3. ProvingJML Contracts: This chapter explains how to apply your knowledge from the previous chapter, showing how KeY generates proof obligations and how to prove them.
  4. Appendix

Bibliography

  1. Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt, and Mattias Ulbrich, editors. Deductive Software Verification - The KeY Book - From Theory to Practice. Volume 10001 of Lecture Notes in Computer Science. Springer, December 2016. ISBN 978-3-319-49811-9. doi:10.1007/978-3-319-49812-6. ↩

  2. Dominic Steinhöfel and Reiner Hähnle. Abstract Execution, pages 319–336. Springer, Berlin, October 2019. URL: http://tubiblio.ulb.tu-darmstadt.de/117206/, doi:10.1007/978-3-030-30942-8\_20. ↩

  3. Bernhard Beckert, Reiner Hähnle, and Peter H. Schmitt, editors. Verification of Object-Oriented Software: The KeY Approach. LNCS 4334. Springer-Verlag, 2007. ↩

  4. Bernhard Beckert and Christoph Gladisch. White-box testing by combining deduction-based specification extraction and black-box testing. In B. Meyer and Y. Gurevich, editors, Proceedings, International Conference on Tests and Proofs (TAP), Zurich, Switzerland, LNCS 4454. Springer, 2007. ↩

  5. Steffen Schlager. Symbolic Execution as a Framework for Deductive Verification of Object-Oriented Programs. PhD thesis, Fakultät für Informatik der Universität Karlsruhe, February 2007. ↩

  6. Andreas Roth. Specification and Verification of Object-oriented Components. PhD thesis, Fakultät für Informatik der Universität Karlsruhe, June 2006. ↩

  7. Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen Schlager, and Peter H. Schmitt. The KeY tool. Software and System Modeling, 4:32–54, 2005. doi:http://springerlink.metapress.com/openurl.asp?genre=article&id=doi:10.1007/s10270-004-0058-x. ↩

  8. Bernhard Beckert. A dynamic logic for the formal verification of Java Card programs. In I. Attali and T. Jensen, editors, Java on Smart Cards: Programming and Security. Revised Papers, Java Card 2000, International Workshop, Cannes, France, LNCS 2041, 6–24. Springer-Verlag, 2001. ↩

  9. Steffen Schlager. Handling of Integer Arithmetic in the Verification of Java Programs. Master's thesis, Universität Karlsruhe, 2002. Available at: \url http://i12www.ira.uka.de/ key/doc/2002/DA-Schlager.ps.gz. ↩

  10. Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen Schlager, and Peter H. Schmitt. The Key Tool. Technical Report in Computing Science No. 2003-5, Department of Computing Science, Chalmers University and Göteborg University, Göteborg, Sweden, February 2003. Available at: \url http://i12www.ira.uka.de/ beckert/pub/key03.pdf. ↩

  11. ESC/Java (Extended Static Checking for Java). \url http://research.compaq.com/SRC/esc/. ↩

  12. Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Wolfram Menzel, and Peter H. Schmitt. The KeY approach: Integrating object oriented design and formal verification. In Manuel Ojeda-Aciego, Inma P. de Guzmán, Gerhard Brewka, and Lu\'ıs Moniz Pereira, editors, Proc. 8th European Workshop on Logics in AI (JELIA), Malaga, Spain, volume 1919 of LNCS, 21–36. Springer-Verlag, October 2000. ↩

  13. Bertrand Meyer. Object-Oriented Software Construction (Second Edition). Pren­tice-Hall, 1997. ↩

  14. Gary T. Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, Peter Müller, Joseph Kiniry, Patrice Chalin, and Daniel M. Zimmerman. Jml reference manual. Department of Computer Science, Iowa State University. Available from \url http://www.jmlspecs.org, July 2011. ↩

  15. Gary T. Leavens, Albert L. Baker, and Clyde Ruby. Preliminary design of JML: a behavioral interface specification language for Java. Technical Report 98-06y, Iowa State University, Department of Computer Science, November 2004. See \url http://www.jmlspecs.org. URL: ftp://ftp.cs.iastate.edu/pub/techreports/TR98-06/TR.ps.gz. ↩

  16. Thomas Baar, Reiner Hähnle, and Steffen Schlager. Key quicktour. See \url http://www.key-project.org/download/. ↩

  17. \url http://www.icansolve.com. ↩

  18. \url http://secure.ucd.ie/products/opensource/ESCJava2/. ↩

  19. JavaRedux - API. API documentation of a restricted subset of the Java Standard Library Classes. URL: https://git.key-project.org/key-public/key/-/tree/stable/key/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux. ↩

  20. Clark Barrett, Silvio Ranise, Aaron Stump, and Cesare Tinelli. The Satisfiability Modulo Theories Library (SMT-LIB). \tt www.SMT-LIB.org, 2008. ↩

  21. Christian Engel and Reiner Hähnle. Generating unit tests from formal proofs. In Bertrand Meyer and Yuri Gurevich, editors, Proc. Tests and Proofs (TAP), Zürich, Switzerland, volume 4454 of LNCS. Springer-Verlag, 2007. ↩

  22. Christian Engel. A translation from jml to java dynamic logic. Studienarbeit, Fakultät für Informatik, Universität Karlsruhe, January 2005. ↩

  23. Benjamin Weiß. Deductive Verification of Object-Oriented Software: Dynamic Frames, Dynamic Logic and Predicate Abstraction. PhD thesis, Karlsruhe Institute of Technology, 2011. ↩