From 85e6c1fb64f7f863eaa42bbda3031645b51d9674 Mon Sep 17 00:00:00 2001 From: Drodt Date: Mon, 20 Jul 2026 14:12:07 +0200 Subject: [PATCH] Add FM24 Tutorial to Example dialog (and fix typo) --- .../heap/FM2024Tutorial/ArrayList/README.txt | 15 +++++++++++++++ .../heap/FM2024Tutorial/BinarySearch/README.txt | 11 +++++++++++ key.ui/examples/heap/removeDups/README.txt | 2 +- key.ui/examples/index/samplesIndex.txt | 4 ++++ 4 files changed, 31 insertions(+), 1 deletion(-) create mode 100644 key.ui/examples/heap/FM2024Tutorial/ArrayList/README.txt create mode 100644 key.ui/examples/heap/FM2024Tutorial/BinarySearch/README.txt diff --git a/key.ui/examples/heap/FM2024Tutorial/ArrayList/README.txt b/key.ui/examples/heap/FM2024Tutorial/ArrayList/README.txt new file mode 100644 index 00000000000..57460ce5ac4 --- /dev/null +++ b/key.ui/examples/heap/FM2024Tutorial/ArrayList/README.txt @@ -0,0 +1,15 @@ +example.name = Array List and Linked List +example.path = FM 2024 Tutorial +example.additionalFile.1 = src/List.java +example.additionalFile.2 = src/ArrayList.java +example.additionalFile.3 = src/Node.java +example.additionalFile.4 = src/LinkedList.java +example.additionalFile.5 = src/Test.java + +The binary search examples from the paper "The Java verification tool KeY: A tutorial" presented as the Formal Methods Symposium 2024 in Milan. + +@author Bernhard Beckert, Richard Bubel, Daniel Drodt, Reiner Hähnle, Florian Lanzinger, Wolfram Pfeifer, Mattias Ulbrich, Alexander Weigl + +This example contains an interface for a List with operations "size", "get", "add", and "find." The interface is implemented as an ArrayList and a LinkedList of Nodes and highlights the usage of ghost fields and dynamic frames. + +Some proofs need manual proof interaction to close. \ No newline at end of file diff --git a/key.ui/examples/heap/FM2024Tutorial/BinarySearch/README.txt b/key.ui/examples/heap/FM2024Tutorial/BinarySearch/README.txt new file mode 100644 index 00000000000..c11d876b7b0 --- /dev/null +++ b/key.ui/examples/heap/FM2024Tutorial/BinarySearch/README.txt @@ -0,0 +1,11 @@ +example.name = Binary Search +example.path = FM 2024 Tutorial +example.additionalFile.1 = src/BinSearch.java + +The binary search examples from the paper "The Java verification tool KeY: A tutorial" presented as the Formal Methods Symposium 2024 in Milan. + +@author Bernhard Beckert, Richard Bubel, Daniel Drodt, Reiner Hähnle, Florian Lanzinger, Wolfram Pfeifer, Mattias Ulbrich, Alexander Weigl + +Binary search returns the index of a given element in a sorted array if it exists. + +The example contains two implementations of binary search: recursive and iterative. The former return -1 if the element is not found; the latter throws an exception in that case. Both example close without user interaction. \ No newline at end of file diff --git a/key.ui/examples/heap/removeDups/README.txt b/key.ui/examples/heap/removeDups/README.txt index 8ddcce3b664..81bb68aa765 100644 --- a/key.ui/examples/heap/removeDups/README.txt +++ b/key.ui/examples/heap/removeDups/README.txt @@ -3,7 +3,7 @@ example.path = Getting Started example.additionalFile.1 = RemoveDup.unspecified example.additionalFile.2 = RemoveDup.java -This is a simple excercise for JML and KeY. +This is a simple exercise for JML and KeY. @author Mattias Ulbrich diff --git a/key.ui/examples/index/samplesIndex.txt b/key.ui/examples/index/samplesIndex.txt index afa89037598..666003ded24 100644 --- a/key.ui/examples/index/samplesIndex.txt +++ b/key.ui/examples/index/samplesIndex.txt @@ -20,6 +20,10 @@ firstTouch/09-Quicktour/README.txt firstTouch/10-SITA/README.txt firstTouch/11-StateMerging/README.txt +# FM 2024 Tutorial +heap/FM2024Tutorial/BinarySearch/README.txt +heap/FM2024Tutorial/ArrayList/README.txt + # Java Features Java/MultiCatch/README.txt Java/Records/README.txt