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
7 Formal Specification with the Java Modeling Language All Examples
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