updated README

README.md

@@ -21,7 +21,7 @@ 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 (ArrayList and LinkedList) that showcase how data structures can be specified and verified in KeY.
+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.
 
 Both examples comprise:
 * `src`: a directory containing the Java source files, annotated with JML specifications
@@ -39,11 +39,11 @@ If you want to run KeY interactively, the KeY UI can be started by launcing the
 ```
 $ java -jar tools/key-2.13.0-exe.jar
 ```
+or using the shell script `startkey.sh` in the toplevel directory.
 
 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).
 
-
-[^1] It may be that you have to close the example choice window first.
+[^1]: It may be that you have to close the example choice window first.
 
 ### Verifying from the commandline
 
@@ -67,7 +67,7 @@ Deadline: next kakey meeting, 21.06.2024
 * MU:
   * Readme
     * [x] Add link to the FM tutorial webpage
-    * Description of the both case studies.
+    * [x] Description of the two case studies.
     * [x] Interactive use
   * [x] Beweis von sort()
   * [x] Beweis von List::add():