Skip to content

Commit 4a39b67

Browse files
committed
added quicksort as jml proof script reference
1 parent beeaeef commit 4a39b67

File tree

1 file changed

+4
-0
lines changed
  • docs/workbench/Proof Scripts

1 file changed

+4
-0
lines changed

docs/workbench/Proof Scripts/jml.md

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -150,6 +150,10 @@ Here are some examples of proof scripts in JML:
150150

151151
see https://github.com/KeYProject/key/blob/96a6a98328bb9dbaadfb5b54e11b29230e77dfe9/key.ui/examples/heap/BoyerMoore/src/BoyerMoore.java
152152

153+
### Proof of Quicksort using JML proof scripts
154+
155+
see https://github.com/KeYProject/key/blob/4579ddf083e76927db5c2ffb40268962482aa9e3/key.ui/examples/heap/quicksort/Quicksort.java
156+
153157
### Proof of the [IPS4O sorting algorithm](https://doi.org/10.1007/978-3-031-57246-3_15) (partially) using scripts
154158

155159
see https://github.com/KeYProject/ips4o-verify/blob/pfeifer/STTT/src/main/java/de/wiesler/Sorter.java

0 commit comments

Comments
 (0)