 | This article is written like a personal reflection, personal essay, or argumentative essay that states a Wikipedia editor's personal feelings or presents an original argument about a topic.(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.
One of the first occurrences of Meta-IV in print appears to be "Programming in the Meta-language: A Tutorial". [1] 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*. [2] 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 passage [3]
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 [4] which existed (and to some extent still do) from the 1970s onwards:
A brief account of these different Schools is given in the text "Mathematical Approaches to Software Quality". [6]
A comprehensive VDM Bibliography [7] is also available.
founded by Dines Bjørner
To mention:
founded by Cliff Jones (computer scientist)
To mention:
founded by Mícheál Mac an Airchinnigh
To mention:
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. [8] 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. [9]
Other substantial works related to the School are also online. [10]
The three Schools were brought under a common organizational structure called VDM Europe [11] 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 [12] in favor of Formal Methods Europe, founded in 1992. [13] Minutes of the first meeting of FME are available online. [14]
List of the VDM and FME conferences (http://www.informatik.uni-trier.de/~ley/db/conf/fm/)
{{cite web}}: CS1 maint: archived copy as title (link){{cite web}}: CS1 maint: archived copy as title (link){{cite web}}: CS1 maint: archived copy as title (link)
The Unified Modeling Language (UML) is a general-purpose, developmental modeling language in the field of software engineering that is intended to provide a standard way to visualize the design of a system.
The Z notation is a formal specification language used for describing and modelling computing systems. It is targeted at the clear specification of computer programs and computer-based systems in general.
The Vienna Development Method (VDM) is one of the longest-established formal methods for the development of computer-based systems. Originating in work done at the IBM Laboratory Vienna in the 1970s, it has grown to include a group of techniques and tools based on a formal specification language—the VDM Specification Language (VDM-SL). It has an extended form, VDM++, which supports the modeling of object-oriented and concurrent systems. Support for VDM includes commercial and academic tools for analyzing models, including support for testing and proving properties of models and generating program code from validated VDM models. There is a history of industrial usage of VDM and its tools and a growing body of research in the formalism has led to notable contributions to the engineering of critical systems, compilers, concurrent systems and in logic for computer science.
In computer science, formal methods are mathematically rigorous techniques for the specification, development, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.
The B method is a method of software development based on B, a tool-supported formal method based on an abstract machine notation, used in the development of computer software.
In computer science, formal specifications are mathematically based techniques whose purpose are to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verifying key properties of interest through rigorous and effective reasoning tools. These specifications are formal in the sense that they have a syntax, their semantics fall within one domain, and they are able to be used to infer useful information.
Clifford "Cliff" B. Jones is a British computer scientist, specializing in research into formal methods. He undertook a late DPhil at the Oxford University Computing Laboratory under Tony Hoare, awarded in 1981. Jones' thesis proposed an extension to Hoare logic for handling concurrent programs, rely/guarantee.
Professor Dines Bjørner is a Danish computer scientist.
RAISE was developed as part of the European ESPRIT II LaCoS project in the 1990s, led by Dines Bjørner. It consists of a set of tools designed for a specification language (RSL) for software development. It is especially espoused by UNU-IIST in Macau, who run training courses on site and around the world, especially in developing countries.
Zhou Chaochen is a Chinese computer scientist.
BCS-FACS is the BCS Formal Aspects of Computing Science Specialist Group.
Formal Methods Europe (FME) is an organization whose aim is to encourage the research and application of formal methods for the improvement of software and hardware in computer-based systems. The association's members are drawn from academia and industry. It is based in Europe, but is international in scope. FME operates under Dutch law.
John S. Fitzgerald FBCS is a British computer scientist. He is a professor at Newcastle University. He was the head of the School of Computing before taking on the role of Dean of Strategic Projects in the university’s Faculty of Science, Agriculture and Engineering. His research interests are in the area of dependable computer systems and formal methods, with a background in the VDM. He is a former Chair of Formal Methods Europe and committee member of BCS-FACS.
Prentice Hall International Series in Computer Science was a series of books on computer science published by Prentice Hall.
Model-based specification is an approach to formal specification where the system specification is expressed as a system state model. This state model is constructed using well-understood mathematical entities such as sets and functions. System operations are specified by defining how they affect the state of the system model.
Professor Martin C. Henson FBCS FRSA is an English computer scientist based at the University of Essex. He is dean for international affairs and is affiliated to the School of Computer Science & Electronic Engineering. Henson was head of the department of computer science from 2000 to 2006.
DDC-I, Inc. is a privately held company providing software development of real-time operating systems, software development tools, and software services for safety-critical embedded applications, headquartered in Phoenix, Arizona. It was first created in 1985 as the Danish firm DDC International A/S, a commercial outgrowth of Dansk Datamatik Center, a Danish software research and development organization of the 1980s. The American subsidiary was created in 1986. For many years, the firm specialized in language compilers for the programming language Ada.
Dansk Datamatik Center (DDC) was a Danish software research and development centre that existed from 1979 to 1989. Its main purpose was to demonstrate the value of using modern techniques, especially those involving formal methods, in software design and development.
IBM Laboratory Vienna was an IBM research laboratory based in Vienna, Austria.
Peter Lucas was an Austrian computer scientist and university professor.