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.