Mondex in VDM++

Latest Status

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, Ether 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).

Participants

ZoeAndrews, Steve Riddle, JohnFitzgerald, JeremyBryans, KenPierce, JohnHughes, RichardPayne, SarahClarke.

An overview of Mondex by Ken

• Newcastle_Mondex_12th_February_2007_(K.G.Pierce).ppt: Ken's slides 12th Feb 2007

Actions

• 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

Proof Effort

The following is a list of proof obligations that make up the proof effort for the VDM-SL specification.

Rule	Resp.	Done	Typeset	Check1	Check2
inv-ConWorld-form	Completed	Yes	Yes	Yes	Yes
ConWorld-1-form	Completed	Yes	Yes	Yes	Yes
retr-form	Completed	Yes	Yes	Yes	Yes
dom-purses-=	Completed	Yes	Yes	Yes	Yes
bal-purses-equal	Completed	Yes	Yes	Yes	Yes
\delta-pre-AbTransferLost	Completed	Yes	Yes	Yes	Yes
+-=	Completed	Yes	Yes	Yes	Yes
ConWorld-AbWorld-form	Completed	Yes	Yes	Yes	Yes
\delta->=	Completed	Yes	Yes	Yes	Yes
post-dom-=	Completed	Yes	Yes	Yes	Yes
post-abauth-=	Completed	Yes	Yes	Yes	Yes
TransferLost-res	JeremyBryans	Yes	Yes	Yes	No
sumval-form	JohnFitzgerald	Yes	Yes	No	No
comp-set-ind	JohnFitzgerald	Yes	No	No	No
TransferLost-dom	JohnFitzgerald	Yes	Yes	Yes	No
retr-adequate	JohnFitzgerald	Yes	Yes	No	No
auth-=	JohnFitzgerald	Yes	Yes	No	No
con-assign	JohnFitzgerald	Yes	Yes	No	No
post-forall-=	NOT ZoeAndrews or RichardPayne	Yes	Yes	Yes	No
post-bal-geq	NOT ZoeAndrews or RichardPayne	Yes	Yes	Yes	No
post-total-=	NOT ZoeAndrews or RichardPayne	Yes	Yes	Yes	No
total-C-form	NOT ZoeAndrews or RichardPayne	Yes	Yes	Yes	No
in-eq-set	NOT ZoeAndrews or RichardPayne	Yes	Yes	Yes	No
total-purses-=	NOT ZoeAndrews or RichardPayne	Yes	Yes	Yes	No
at-mk-abpurse-defn	NOT ZoeAndrews or RichardPayne	Yes	Yes	Yes	No
ab-set-form	NOT ZoeAndrews or RichardPayne	Yes	Yes	Yes	No
forall-elem-I	RichardPayne	No	No	No	No
diff-\not-=	ZoeAndrews	Yes	Yes	Yes	No

External resources

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).

-- RichardPayne - 06 Nov 2007