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) 23 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 4. In case of questions or comments, don't hesitate to contact the KeYsupport team at 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. 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. ↩

  2. 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. ↩

  3. 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. ↩

  4. 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. ↩