This page offers downloads of annotated Java programs or KeY problem files used in the book.
| Chapter | Title | Remarks | Download |
|---|---|---|---|
| 7 | Formal Specification with the Java Modeling Language | All Examples | |
| 12 | Proof-based Test Case Generation | All Examples | |
| 15 | Using the KeY Prover | Consult the included README.txt for further information about the contents. | All Examples |
| 16 | Formal Verification with KeY: A Tutorial | Consult the included README.txt file for further explanations. | All Examples |
| PostInc.java | Listing 6.1 in the KeY-book | PostInc.java | |
| PostInc.proof | proof of the only contract in PostInc.java | PostInc.proof | |
| Sort.java | Listing 6.2 in the KeY-book | Sort.java | |
| Sort_max.proof | proof of contract for max in Sort.java | Sort_max.proof | |
| Sort_sort.proof | proof of contract for sort in Sort.java | Sort_sort.proof | |
| SortPerm.java | Listing 6.3 in the KeY-book | SortPerm.java | |
| SortPerm_max.proof | proof of contract for max in SortPerm.java | SortPerm_max.proof | |
| SortPerm_sort.proof | proof of contract for sort in SortPerm.java | SortPerm_sort.proof |
If something should be missing, you can contact us or the author(s) of the corresponding book chapter.