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