Examples from the book

This page is under construction.

This page offers downloads of annotated Java programs or KeY problem files used in the book.

Chapter Title Remarks Download
12 Proof-based Test Case Generation All Examples
15Using the KeY ProverConsult 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