diff --git a/README.md b/README.md index 341f1a2..ba7c7ee 100644 --- a/README.md +++ b/README.md @@ -4,7 +4,7 @@ This repository contains the accompanying material and the tool executables for ## About KeY -The [KeY tool](https://www.key-project.org) is a state-of-the-art deductive program verifier for the Java language. Its verification engine is based on a sequent calculus for dynamic logic, realizing forward symbolic execution of the target program, whereby all symbolic paths through a program are explored. Method contracts make verification scalable, because one can prove one method at a time to be correct relative to its contract. KeY combines auto-active and fine-grained proof interaction which is possible both at the level of the verification target and its specification, as well as at the level of proof rules and program logic. This makes KeY well-suited for teaching program verification, but also permits proof debugging at the source code level. The latter made it possible to verify some of the most complex Java code to date with KeY. [The accompanying article](https://www.key-project.org/LINK_TO_ARTICLE) provides a self-contained introduction to the working principles and the practical usage of KeY for anyone with basic knowledge in logic and formal methods. +The [KeY tool](https://www.key-project.org) is a state-of-the-art deductive program verifier for the Java language. Its verification engine is based on a sequent calculus for dynamic logic, realizing forward symbolic execution of the target program, whereby all symbolic paths through a program are explored. Method contracts make verification scalable, because one can prove one method at a time to be correct relative to its contract. KeY combines auto-active and fine-grained proof interaction which is possible both at the level of the verification target and its specification, as well as at the level of proof rules and program logic. This makes KeY well-suited for teaching program verification, but also permits proof debugging at the source code level. The latter made it possible to verify some of the most complex Java code to date with KeY. [The accompanying article](https://www.key-project.org/wp-content/uploads/2024/06/KeYTutorialFM2024-preprint.pdf) provides a self-contained introduction to the working principles and the practical usage of KeY for anyone with basic knowledge of logic and formal methods. ## Material @@ -20,8 +20,8 @@ The page at [`www.key-project.org/tutorial-fm-2024`](https://www.key-project.org This tutorial repository contains two examples on proving programs correct with KeY: -1. `BinarySearch` – contains the simple example of a binary search implementation looking for an integer value in an array. This is the running example used in the article. It covers an imperative and a recursive implementation. -2. `ArrayList` – contains a straightforward List interface together with two implementations that showcase how data structures can be specified and verified in KeY. The interface defines a few methods methods (`add`, `get`, `size` and `find`) typical for lists. A ghost variable `seq` that models the abstract value of the list. An implementation `ArrayList` shows how a random-access implementation can realize these functionalities. The class `LinkedList` (together with `Node`) show a linked list implementation can be specified and verified. There is a ghost field `footprint` used to model the framing condition using dynamic frames. +1. `BinarySearch` – contains a simple example of a binary search implementation looking for an integer value in an array. This is the running example used in the article. It covers an imperative and a recursive implementation. +2. `ArrayList` – contains a straightforward List interface together with two implementations that showcase how data structures can be specified and verified in KeY. The interface defines a few methods (`add`, `get`, `size`, and `find`) typical for lists. A ghost variable `seq` that models the abstract value of the list. An implementation `ArrayList` shows how a random-access implementation can realize these functionalities. The class `LinkedList` (together with `Node`) shows a linked list implementation can be specified and verified. There is a ghost field `footprint` used to model the framing condition using dynamic frames. Both examples comprise: * `src`: a directory containing the Java source files, annotated with JML specifications @@ -41,7 +41,7 @@ $ java -jar tools/key-2.13.0-exe.jar ``` or using the shell script `startkey.sh` in the toplevel directory which suppresses some log messages. -When the UI opens[^1] you can load a project (via the menu File > Open). Choose one of the `project.key` files from the example directories to load one of the two examples. A window will open afterwards from which you can choose which contract you would like to verify. For an introduction and tips on how to use the system, see the tutorial notes and videos for details (links at the tutorial page mentioned above). +When the UI opens[^1] you can load a project (via the menu `File > Open`). Choose one of the `project.key` files from the example directories to load one of the two examples. A window opens afterward from which you can choose which contract you would like to verify. For an introduction and tips on how to use the system, see the tutorial notes and videos for details (links at the tutorial page mentioned above). [^1]: It may be that you have to close the example choice window first.