Skip to content

Commit 44fa02a

Browse files
committed
added red-black-trees as example in jml proof scripts
1 parent a3dbcb3 commit 44fa02a

File tree

1 file changed

+4
-0
lines changed

1 file changed

+4
-0
lines changed

docs/user/ProofScripts/jml.md

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -154,6 +154,10 @@ see https://github.com/KeYProject/key/blob/96a6a98328bb9dbaadfb5b54e11b29230e77d
154154

155155
see https://github.com/KeYProject/key/blob/4579ddf083e76927db5c2ffb40268962482aa9e3/key.ui/examples/heap/quicksort/Quicksort.java
156156

157+
### Proof of Red-Black-Trees using JML proof scripts
158+
159+
see https://github.com/KeYProject/rbtree-verification/blob/main/src/Tree.java
160+
157161
### Proof of the [IPS4O sorting algorithm](https://doi.org/10.1007/978-3-031-57246-3_15) (partially) using scripts
158162

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

0 commit comments

Comments
 (0)