Mondex in VDM++
The abstract and concrete models have been proposed in executable VDM++, plus pre/post specifications and are presented here. The abstract model consists of an Abstract Purse
and an Abstract World
. The concrete model is made up of a Concrete Purse
, Concrete World
and Perfect Ether
. To prove properties of the models, flattened VDM-SL versions have been produced, consisting of a Concrete World
and an Abstract World
Following some tutorials on proof (given by John), we've started hand-proofs of refinement. Again, we have been concentrating on spreading proof skills in the group and involving as many folk as possible. The totality and adequecy proofs are completed, and we are in the process of typesetting these. We are now concentrating on the domain and result proofs.
We intend to set up the VDM->HOL environment developed by SanderVermolen
. This has already been used to discharge the consistency proof obligations of a VDM-SL version of the abstract Mondex model. We'll look to apply it to the concrete model and to the refinement proof obligation (or at least the major lemmas of that).
We are in the process of experimenting with the combinatorial testing capabilities of Overture for the abstract model. We have completed traces which test the preconditions of the AbWorld transfer operations, and are looking into ways to test the (strong) post-conditions and class invariant.
, Steve Riddle, JohnFitzgerald
An overview of Mondex by Ken
- We wish to be able to use SanderVermolen’s VDM->HOL environment to discharge the proof obligations of the concrete model produced. This requires the setting up of the proof generator, and subsequently learning to work with HOL.
- We wish to produce a student crib-sheet style document for 2nd year students studying VDM++. This documents brings together the fundamental concepts in a short guide
- Hand proofs for domain and result
- Produce outline for possible paper on VDM Mondex approach
- Develop a graphical user interface for interaction with the Mondex model, MondexGui
- Experiment with the combinatorial testing capabilities of Overture for both the abstract and concrete models.
The following is a list of proof obligations that make up the proof effort for the VDM-SL specification.
A link to Richard Banach's slides on retrenchments: http://www.jiscmail.ac.uk/files/VSR-CONTRIBUTORS/SecondMondexWorkshop/banach.pdf
Slide 93 onwards contains the discussion Ken was talking about. It's in relation to the 'missing' balance enquiry operation (it's not included in the Z) The diagrams should help.
Slides from the other meetings are at http://isegserv.itd.rl.ac.uk/gc6wiki/ThirdMondexWorkshopAgenda
(from October, with latest results) and http://isegserv.itd.rl.ac.uk/gc6wiki/SecondMondexWorkshopAgenda
(from May, intermediate results).
Below are the final FACS papers on six approaches
- 06 Nov 2007