From 38e33af555624a7877c8ffded234ceecf9434fd2 Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Sat, 15 Jun 2024 12:13:27 +0200 Subject: [PATCH] updating README --- README.md | 61 +++++++++++++++++++++++++++++++++++-------------------- 1 file changed, 39 insertions(+), 22 deletions(-) diff --git a/README.md b/README.md index 0fffa71..0e5335e 100644 --- a/README.md +++ b/README.md @@ -1,44 +1,64 @@ # KeY Tool Tutorial, FM 2024 -This repository contains the accompanying material and the tool executables for the KeY tutorial at [Formal Methods 2024](https://www.fm24.polimi.it/) +This repository contains the accompanying material and the tool executables for the KeY tutorial given at [Formal Methods 2024](https://www.fm24.polimi.it/). -The KeY tool 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 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. +## 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. + +## Material Video material extening the tutorial can be found [here](https://www.key-project.org/tutorial-fm-2024/). The accompanying article can be downloaded [here](https://www.key-project.org/wp-content/uploads/2024/06/KeYTutorialFM2024-preprint.pdf). -This tutorial covers two small examples: +The current version of KeY, any news and information is available on its homepage [`www.key-project.org`](https://www.key-project.org). -* `BinarySearch/src` -- contains an example implementation of a binary search for an integer value in an array. -* `ArrayList/src` -- contains an example implementation of List interface together with an +The page at [`www.key-project.org/tutorial-fm-2024`](https://www.key-project.org/tutorial-fm-2024) accompanying this tutorial also covers an interactive video tutorial using the material of this repository. -Additionally, we provide in this artifact the proofs for all proof obligations in the sub-folder `*/proofs`. +## This repository -We also provide a copy of the current working KeY and version: You can easily use `make`: +This tutorial repository contains two examples on proving programs correct with KeY: -``` -$ java -jar tools/key-2.13.0-exe.jar # to start 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 (ArrayList and LinkedList) that showcase how data structures can be specified and verified in KeY. -Beschreiben wie man die Projekte startet. +Both examples comprise: +* `src`: a directory containing the Java source files, annotated with JML specifications +* `project.key`: A KeY input file describing the settings etc. for the resp. example +* `prove.sh`: A shell script to re-run the verification on the command line. +* `proofs` (ArrayList only): Proofs that require interaction are stored here for loading or replay. +The directory `tools` contains the version of KeY to be used for the tutorial. -``` -$ cd BinarySearch; ./prove.sh # verify binary search -``` +## Running the tool +### Interactively + +If you want to run KeY interactively, the KeY UI can be started by launcing the jar file, e.g., using the command ``` -$ cd ArrayList; ./prove.sh # verify the array list +$ java -jar tools/key-2.13.0-exe.jar ``` +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). -This artifact is monitored by continous integration pipeline. +[^1] It may be that you have to close the example choice window first. +### Verifying from the commandline -**License: GPL-v2-only** +In case you want to verify the examples fully automatically from the command line, the repository also contains linux shell scripts that can do this. +You can use the command +``` +$ cd BinarySearch; ./prove.sh +``` +for the binary search example and the command +``` +$ cd ArrayList; ./prove.sh +``` +for the list example. +**License: GPL-v2-only** ## TODOs @@ -46,9 +66,9 @@ Deadline: next kakey meeting, 21.06.2024 * MU: * Readme - * Add link to the FM tutorial webpage + * DONE Add link to the FM tutorial webpage * Description of the both case studies. - * Interactive use + * DONE Interactive use * DONE: Beweis von sort() * DONE: Beweis von List::add(): @@ -69,6 +89,3 @@ Deadline: next kakey meeting, 21.06.2024 Test::test() w/o Z3 - - -