Example: Allocate (Video Version / Fully Proved Version)

This file contains the example as presented in the video of the lecture.

Updated 5, 2019

Example: Books V1 (Video Version)

This file contains the example as presented in the video of the lecture.

Updated 5, 2019

Example: Books V2 (Fully Proved Version)

This file also contains the pmm file that can be used to fully prove the proof obligations of the example. Furthermore, it contains small changes in the REFINEMENT components that were needed to complete these proofs. These changes are described in the source file as comments.

Updated 5, 2019

Example: Jukebox (Video Version / Fully Proved Version)

This file contains the example as presented in the video of the lecture. This file also contains the pmm file that can be used to fully prove the proof obligations of the example.

Updated 5, 2019

Example: MySet V1 (Video Version)

This file contains the example as presented in the video of the lecture.

Updated 5, 2019

Example: MySet V2 (Fully Proved Version)

This file also contains the pmm file that can be used to fully prove the proof obligations of the example. Furthermore, it contains small changes in the MACHINE and REFINEMENT components that were needed to complete these proofs. These changes are described in the source file as comments.

Updated 5, 2019