The B-Method Lecture 11: Data Refinement - Part I

Lecture 11: Data Refinement - Part I

155 Views

This lecture presents the main concepts of data refinement, that is, how to transform data from an abstract mathematical representation into a more concrete data structure.

Supplementary material

Example: Team (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 1, 2019

Example: Exam (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 1, 2019

Example: Ironing V1 (Video Version - Partially 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 partially prove the proof obligations of the example.

Updated 1, 2019

Example: Ironing 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 component that were needed to simplify the proofs. These changes are described in the source file as comments.

Updated 1, 2019

Example: Port (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 1, 2019

More videos

Sign in to receive news from MOOC IMD and to access course forums.