Path: utzoo!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!tut.cis.ohio-state.edu!ucbvax!DURHAM.AC.UK!Barry.Cornelius From: Barry.Cornelius@DURHAM.AC.UK Newsgroups: comp.lang.modula2 Subject: Re: Re: Re: VDM & M2 Message-ID: Date: 16 Feb 90 18:22:58 GMT Sender: daemon@ucbvax.BERKELEY.EDU Reply-To: Modula2 List Organization: The Internet Lines: 55 Randy Bush writes: :Barry writes: : :> Tom states that VDM is a "non-standard language". VDM is currently :> being standardised by ISO, and the VDM standard will define a language :> which currently has the name VDM-SL. : :Ahh, then you agree with Tom that it is not a standard language. Whether it :will someday be so is not very helpful to those trying to interpret the :Modula-2 DP now. Randy, I think you were being unfair to me. I was not meant to be criticising what Tom Reid said. I was just trying to give some more information about the current status of VDM-SL, and how it was intended to use the standard version of VDM when it gets released. Randy also writes: :When one gets the Modula-2 DP, is there any easily obtainable documet which :defines and describes precisely the notation used in the DP? If so, could you :please post info on how we may obtain it esily? Thanks. I believe it makes no sense for us to produce a Standard that is written in a form of VDM that differs from VDM-SL. However, VDM-SL has not yet stabilised and so we have to use some variant of the specification language of VDM in the draft proposal. It also makes no sense for us to spend time formally defining the variant of VDM that we are using because we are going to shift to VDM-SL in the end. (Such work is hard and is really the work of those formally defining VDM-SL.) Therefore we are left with the not very satisfactory but unfortunately not altogether unnecessary state-of-affairs of using a variant of VDM that is not formally defined somewhere. However, Annex D of the Draft Proposal (of the Modula-2 Standard) does give pointers to the variant of VDM being used. It says: [The specification language used in the draft standard] is very similar to the language used in the following books: Systematic Software Development Using VDM C.B.Jones, Prentice-Hall, 1986, 0-13-880717-5 [and:] Software Development: A Rigorous Approach C.B.Jones, Prentice-Hall, 1980, 0-13-821884-6 A particular style of use of the specification language of VDM is often employed when specifying the semantics of programming languages. This style is explained in the book: Formal Specification and Software Development D.Bjorner and C.B.Jones, Prentice-Hall, 1982, 0-13-329003-4 Chapter 4 of this book is particularly useful. I posted this information to the Modula-2 Newsgroup in a recent mailing. == Barry Cornelius == Computer Science Group, School of Engineering and Applied Science, University of Durham, Durham, DH1 3LE, England JANET: Barry.Cornelius@uk.ac.durham Internet: Barry.Cornelius%durham.ac.uk@cunyvm.cuny.edu UUCP: ...ukc!cs.nott.ac.uk!bjc BITNET/EARN: Barry.Cornelius%DURHAM@AC.UK Tel: Durham (091 or +44 91) 374 2638, Secretary: 374 2630, Fax: 374 3741