Mondex case study including libraries for data refinement

The original case study can be found on the web:

The technical report describing the KIV case study in more detail can be found here . This work was also published at Formal Methods 2006, the bib entry is:

@InProceedings{kiv-mondex-fm2006,
author = {Gerhard Schellhorn and Holger Grandy and Dominik Haneberg and Wolfgang Reif},
title = {{The Mondex Challenge: Machine Checked Proofs for an Electronic Purse}},
booktitle = {Formal Methods 2006, Proceedings},
year = 2006,
publisher = {Springer},
pages = {16--31},
series = {LNCS},
volume = {4085},
editor = {J. Misra and T. Nipkow and E. Sekerinski },
note = {}
}

The case study is organized in three projects, Mondex (containing the case study itself), Z-Refinement (containing the theory of refinement in Z) and DataRef (containing the theory of Data Refinement of Hoare and He as well the theory of refinement of the contract approach).

Mondex

The main specifications are:

Z-Refinement:

Data Refinement

 Data Refinement according to Hoare / He: Data Refinement using the contract approach and invariants:

[Impressum] [E-Mail]