Meta-IV (specification language)
{{Essay-like|date=January 2018}}
The Meta-IV (pronounced like "metaphor") was an early version of the specification language of the Vienna Development Method formal method for the development of computer-based systems.
History
One of the first occurrences of Meta-IV in print appears to be
"Programming in the Meta-language: A Tutorial".Bjørner&Jones 1978, p24.
Dines Bjørner used it in the very beginning of his tutorial as a footnote
This paper provides an informal introduction to the "art" of abstractly specifying software architectures using the VDM meta-language*.* colloquially known as: META-IV, Bjørner&Jones 1978, p24. A formal treatment of the semantics, as well as a BNF-like concrete syntax, of a large subset of the meta-language is given in [Jones 78a] following this paper.
The spirit of the Meta-IV specification language is well captured by the following passageBjørner&Jones 1978, p33
We stress here... that the meta-language is to be used, not for solving algorithmic problems (on a computer), but for specifying, in an implementation-independent way, the architecture (or models) of software. Instead of using informal English mixed with technical jargon, we offer you a very-high-level 'programming' language. We do not offer an interpreter or compiler for this meta-language. And we have absolutely no intention of ever wasting our time trying to mechanize this meta-language. We wish, as we have done in the past, and as we intend to continue doing in the future, to further develop the notation and to express notions in ways for which no mechanical interpreter system can ever be provided.
VDM is a Method. The Meta-IV was the Specification language that accompanied the method, and the VDM-SL is the current standardized form of that language.
Since the VDM-SL has become standardized, then one may use Meta-IV to denote the three specific Schools of
the VDM{{Cite web |url=http://www.vdmportal.org/twiki/pub/Main/WebHome/bjorner-vdm-ipsj-20oct06.pdf |title=Archived copy |access-date=2008-05-05 |archive-url=https://web.archive.org/web/20090106190947/http://www.vdmportal.org/twiki/pub/Main/WebHome/bjorner-vdm-ipsj-20oct06.pdf |archive-date=2009-01-06 |url-status=dead }} which existed (and to some extent still do) from the 1970s onwards:
- The Danish School — founded by [http://www2.imm.dtu.dk/~db/ Dines Bjørner]
- The English School — founded by [https://web.archive.org/web/20100731082829/http://www.cs.ncl.ac.uk/people/cliff.jones/ Cliff Jones]
- The Irish School[http://portal.acm.org/author_page.cfm?id=81100168285&coll=GUIDE&dl=GUIDE&trk=0&CFID=26571118&CFTOKEN=15016975 Micheal Mac an Airchinnigh - ACM author profile page] — founded by [https://tcdlocalportal.tcd.ie/pls/webapps/cerif.cerif_cv.display_cv?p_cv_id=688 Mícheál Mac an Airchinnigh]{{dead link|date=January 2018 |bot=InternetArchiveBot |fix-attempted=yes }}
A brief account of these different Schools is given in the text "Mathematical Approaches to Software Quality".O'Regan 2006
A comprehensive VDM BibliographyGorm Larsen, Peter is also available.
The Schools of VDM
=The Danish School=
founded by Dines Bjørner
To mention:
- Technical University of Denmark (DTU) in Lyngby
- Dansk Datamatik Center (DDC)
=The English School=
founded by Cliff Jones (computer scientist)
To mention:
- University of Manchester
- University of Newcastle
=The Irish School=
founded by Mícheál Mac an Airchinnigh
To mention:
- University of Dublin, Trinity College
The first appearance of the name "Irish School of the VDM" occurs in a PhD Thesis:
Mac an Airchinnigh, Mícheál. Conceptual Models and Computing.[https://www.cs.tcd.ie/Micheal.MacanAirchinnigh/Web%20Pages/ME_FEIN/SCRIBHNEOIREACHT/FOILSEACHAN/Master.html Foilseacháin] {{webarchive|url=https://web.archive.org/web/20040821230702/http://www.cs.tcd.ie/Micheal.MacanAirchinnigh/Web%20Pages/ME_FEIN/SCRIBHNEOIREACHT/FOILSEACHAN/Master.html |date=2004-08-21 }} Ph.D. Thesis. University of Dublin, Trinity College, Dublin, 1990, p. 41:
There is essential universal agreement on what constitutes the VDM. However, there are basically two major Schools of the VDM largely
distinguished by notational differences employed in the specification language Meta-IV — the Danish School and the English School."
and further down on the same page
There is also the Polish School, which finds expression through the MetaSoft project (Blikle 1987, 1988, 1990). I will frequently need to distinguish between the style of notation and method that I use from those of the other Schools of the VDM. I presume to use the phrase 'the Irish School of the VDM' to draw that distinction.
The Thesis is available online.[https://www.cs.tcd.ie/Andrew.Butterfield/IrishVDM/reading/PhD-MMA.pdf Titlepage]
Other substantial works related to the School are also online.[https://www.cs.tcd.ie/Andrew.Butterfield/IrishVDM/ Irish School of VDM - Home Page]
VDM Europe
The three Schools were brought under a common organizational structure called VDM Europe[http://www.sigmod.org/dblp/db/conf/fm/vdme1987.html VDM Europe 1987] which held it first international conference in Brussels, Belgium, March 23–26, 1987. At the time funding was provided under the Esprit Programme of the European Union.
Meetings were mostly held in the EU Commission buildings in Brussels, Belgium.
VDM Europe eventually was dissolved{{cite web |url=http://www.fmeurope.org/manasite/mas/fme/meetingsitem/30556-757.pdf |title=Archived copy |accessdate=2008-05-05 |url-status=dead |archiveurl=https://web.archive.org/web/20080827163240/http://www.fmeurope.org/manasite/mas/fme/meetingsitem/30556-757.pdf |archivedate=2008-08-27 }} in favor of Formal Methods Europe, founded in 1992.Formal Methods Europe Minutes of the first meeting of FME are available online.{{cite web |url=http://www.fmeurope.org/manasite/mas/fme/meetingsitem/30538-740.pdf |title=Archived copy |accessdate=2008-05-05 |url-status=dead |archiveurl=https://web.archive.org/web/20080827163801/http://www.fmeurope.org/manasite/mas/fme/meetingsitem/30538-740.pdf |archivedate=2008-08-27 }}
Conferences
List of the VDM and FME conferences (http://www.informatik.uni-trier.de/~ley/db/conf/fm/)
Notes
{{Reflist|2}}
Reading Links
- {{cite book | last = Bjørner | first = Dines | authorlink = |author2=Cliff B. Jones | title = The Vienna Development Method: The Meta-Language, Lecture Notes in Computer Science 61 | publisher = Springer | year = 1978 | location = Berlin, Heidelberg, New York | pages = | url = | doi = | id = | isbn = 978-3-540-08766-3 }}
- {{cite book | last = O'Regan | first = Gerard | authorlink = | title = Mathematical Approaches to Software Quality | publisher = Springer | year = 2006 | location = London | pages = | url = | doi = | id = | isbn = 978-1-84628-242-3 }}
- {{Cite book| editor=Cliff B. Jones | title = Programming Languages and Their Definition — H. Bekič (1936-1982)| series = Lecture Notes in Computer Science | volume= 177 | publisher = Springer-Verlag | year = 1984 | location = Berlin, Heidelberg, New York, Tokyo | isbn = 978-3-540-13378-0 | doi = 10.1007/BFb0048933| s2cid = 7488558}}
External links
- {{cite web|url=http://liinwww.ira.uka.de/bibliography/SE/vdm.html |title=The VDM Bibliography |accessdate=2008-08-13 |last=Gorm Larsen |first=Peter }}
- {{cite web|url=http://www.fmeurope.org/ |title=Formal Methods Europe |accessdate=2008-08-13 }}