🚀 go-pugleaf

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