BOTCHAIR@UOGUELPH.BITNET (Alex Bewley) (02/08/90)
I have seen fleeting mentions of Modula having been defined in VDM.
I have been doing a little reading about formal specifications for
complex systems and VDM came up.
Does anyone have examples of VDM code? Especially as it pertains to
languages.
Alex
---------------------------------------------------
BOTCHAIR@UOGUELPH
Alex Bewley -- Just this guy...Barry.Cornelius@DURHAM.AC.UK (02/08/90)
The Draft Proposal for a Modula-2 Standard uses VDM to
specify the semantics of the language formally. The VDM that
is used is close to that used in the following books:
Systematic Software Development Using VDM
C.B.Jones, Prentice Hall, 1986, 0-13-880717-5, 1st edition
and:
Software Development: A Rigorous Approach
C.B.Jones, Prentice Hall, 1980, 0-13-821884-6
(The 1986 Jones book is better than the 1980 book for this work.)
There is a particular style of use of the specification language
of VDM that is 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.
==
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 3741reid@CTC.CONTEL.COM (Tom Reid x4505) (02/09/90)
>From: Alex Bewley <BOTCHAIR%UOGUELPH.BITNET@PSUVM.PSU.EDU> > > I have seen fleeting mentions of Modula having been defined in VDM. > I have been doing a little reading about formal specifications for > complex systems and VDM came up. > Does anyone have examples of VDM code? Especially as it pertains to > languages. I don't want this to be smart-assed, but the new standard has more VDM in it than any mere mortal could wish to read in a millennium. (And the English translation is right next to it.) I appreciate what the advocates of VDM are trying to do but using a non-standard language to try to define an international language standard is stretching things. Get the D106. On a side note. Michael Feldman had to reply to me via the group because he said that my return e-mail address was not included in my posting. I cannot verify this since the mailer does not send me a copy of the messages I send. Can the Modula-2 mailer be changed to echo a copy to the sender? That way, a sender can be sure that the message was forwarded by the exploder. (Of course, I won't know if anyone received this unless someone replies to it!!! :->) Tom.
Barry.Cornelius@DURHAM.AC.UK (02/09/90)
Tom Reid writes: >>I don't want this to be smart-assed, but the new standard has more VDM >>in it than any mere mortal could wish to read in a millennium. (And the >>English translation is right next to it.) I appreciate what the advocates >>of VDM are trying to do but using a non-standard language to try to >>define an international language standard is stretching things. 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. Section 0 Page 1 of the Draft Proposal of the Modula-2 Standard (DP10514, aka D106, aka N336, ...) states that "it is intended that the style [of the VDM used in the Standard] be brought in line with the VDM-SL standard in due course". == 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
rsutc@CS.SFU.CA (rsutc) (02/10/90)
The spec is indeed in VDM. A copy of the spec can be ordered from MODUS. I don't have anything I can transmit to you (easily) except perhaps by faxing. Rick Sutcliffe Associate Professor \ (89-90 only) Visitor Computing Science & Mathematics \ School of Computing Science Trinity Western University \ Simon Fraser University 7600 Glover Rd., \ Burnaby, B.C. Canada V5A 1S6 Langley B.C. Canada V3A 4R9 e-mail: Rick_Sutcliffe@cc.sfu.ca OR Compuserve 76475,3406 Chair: wg13 (modula-2) Canada
rsutc@CS.SFU.CA (rsutc) (02/10/90)
The British were very convincing as they argued that VDM was appropriate for the effort. VDM is itself the subject of a standardization effort. The English of D106 is intended to supplement the VDM, not to be equivalent to it. Rick Sutcliffe Associate Professor \ (89-90 only) Visitor Computing Science & Mathematics \ School of Computing Science Trinity Western University \ Simon Fraser University 7600 Glover Rd., \ Burnaby, B.C. Canada V5A 1S6 Langley B.C. Canada V3A 4R9 e-mail: Rick_Sutcliffe@cc.sfu.ca OR Compuserve 76475,3406 Chairman WG13 (Modula-2) Canada
Pat.Terry@p101.f4.n494.z5.fidonet.org (Pat Terry) (02/12/90)
Hi Tom. When I got it it looked like this > From: reid@CTC.CONTEL.COM (Tom Reid x4505) > Date: 8 Feb 90 16:48:48 GMT > Organization: The Internet > Message-ID: <9002081648.AA06395@ctc.contel.com> > Newsgroups: comp.lang.modula2 > [etc] > That way, a sender can be sure that the message was forwarded by the > exploder. > > (Of course, I won't know if anyone received this unless someone replies to > it!!! :->) > > Tom. > > > --- QM v1.00 > * Origin: Bink of an Aye - Portland, OR US - PEP/V32 (1:105/42.0) > PATH: 494/4 I get it via a FidoNet gate route > -- uucp: uunet!m2xenix!puddle!5!494!4.101!Pat.Terry Internet: Pat.Terry@p101.f4.n494.z5.fidonet.org
randy@m2xenix.UUCP (Randy Bush) (02/13/90)
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. 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. -- ..!uunet!m2xenix!randy randy@psg.com randy@m2xenix.uucp
Barry.Cornelius@DURHAM.AC.UK (02/17/90)
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
reid@CTC.CONTEL.COM (Tom Reid x4505) (02/17/90)
Barry: This really concerns me. We are charged with producing a semanticly correct language standard and you say "It makes no sense for us to spend time formally defining the variant of VDM that we are using ...". If the people who are developing and approving the standard do not (cannot) understand the language that it is being defined in, then we are totally wasting our time. When VDM DOES stabilize and THERE IS a standard reference, THEN it is time to use it to formally define the language. Unless convinced otherwise, I am leaning toward voting against the standard with the VDM left in unless a "reasonable" description of EXACTLY the variant of VDM used is included in the standard. Why do I feel that I am acting out a scene of Alice in Wonderland? Cheers, Tom.
bowen@cs.Buffalo.EDU (Devon Bowen) (02/18/90)
In article <9002170200.AA01479@ctc.contel.com>, reid@CTC.CONTEL.COM (Tom Reid x4505) writes: > When VDM DOES stabilize and THERE IS a standard reference, THEN it is > time to use it to formally define the language. Unless convinced otherwise, > I am leaning toward voting against the standard with the VDM left in unless > a "reasonable" description of EXACTLY the variant of VDM used is included > in the standard. I agree entirely. When the draft arrived here we immediately set out to try implementing it and we have had nothing but trouble since. Using a non-standard language to describe a standard one is the type of thing that anecdotes are made of. What I'm wondering is how difficult is it to ammend a standard? The VDM it currently includes is helpful (once you finally get your hands on one of the references to learn it) but should not be considered the final step. Is there a way the standard can be approved with the intention of revising the VDM later? The difference here is that the implementor can still get something working now but is aware the it will be changing in the future once the semantic technology is in place. On another note, any opinions on the FORWARD statement? Devon
randy@m2xenix.psg.com (Randy Bush) (02/22/90)
I am more confused (no comments from peanut gallery). Surely, you do not intend to imply that, in order to have a published definition of the notation being used in the Modula-2 standard, it will wait for the VDM standardization process (which will take how many years)? -- ..!uunet!m2xenix!randy randy@psg.com randy@m2xenix.uucp