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.