imported>Thekittyburger: /* growthexperiments-addlink-summary-summary:1|2|0 */

2025-11-17T02:22:53Z

growthexperiments-addlink-summary-summary:1|2|0

imported>Cedar101: replace lang="prolog" with lang="rsl" (another formal specification language)

2024-07-24T05:08:44Z

replace lang="prolog" with lang="rsl" (another formal specification language)

Show changes

← Previous revision		Revision as of 02:22, 17 November 2025
Line 1:		Line 1:
	{{short description\|Formal method for the development of computer-based systems}}		{{short description\|Formal method for the development of computer-based systems}}

	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]]<ref>Some idea of that work, including a technical report TR 25.139 on "[https://link.springer.com/content/pdf/10.1007%2FBFb0048942.pdf A Formal Definition of a PL/1 Subset]", dated 20 December 1974, is reprinted in Jones 1984, p.107-155. Of particular note is the list of authors in order: H. Bekič, D. Bjørner, W. Henhapl, C. B. Jones, P. Lucas.</ref> 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++,<ref>The double plus is adopted from the [[C++]] objected oriented programming language based on C.</ref> 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]].		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]]<ref>Some idea of that work, including a technical report TR 25.139 on "[https://link.springer.com/content/pdf/10.1007%2FBFb0048942.pdf A Formal Definition of a PL/1 Subset]", dated 20 December 1974, is reprinted in Jones 1984, p.107-155. Of particular note is the list of authors in order: H. Bekič, D. Bjørner, W. Henhapl, C. B. Jones, P. Lucas.</ref> 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++,<ref>The double plus is adopted from the [[C++]] objected oriented programming language based on C.</ref> which supports the modeling of [[Object-oriented programming\|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]].

	==Philosophy==		==Philosophy==
Line 206:		Line 206:

	====Structuring in VDM-SL====		====Structuring in VDM-SL====
	In the ISO standard for VDM-SL there is an informative annex that contains different structuring principles. These all follow traditional information hiding principles with modules and they can be explained as:		In the ISO standard for VDM-SL there is an informative annex that contains different structuring principles. These all follow traditional [[information hiding]] principles with modules and they can be explained as:
	* '''Module naming''': Each module is syntactically started with the keyword <code>module</code> followed by the name of the module. At the end of a module the keyword <code>end</code> is written followed again by the name of the module.		* '''Module naming''': Each module is syntactically started with the keyword <code>module</code> followed by the name of the module. At the end of a module the keyword <code>end</code> is written followed again by the name of the module.
	* '''Importing''': It is possible to import definitions that has been exported from other modules. This is done in an ''imports section'' that is started off with the keyword <code>imports</code> and followed by a sequence of imports from different modules. Each of these module imports are started with the keyword <code>from</code> followed by the name of the module and a module signature. The ''module signature'' can either simply be the keyword <code>all</code> indicating the import of all definitions exported from that module, or it can be a sequence of import signatures. The import signatures are specific for types, values, functions and operations and each of these are started with the corresponding keyword. In addition these import signatures name the constructs that there is a desire to get access to. In addition optional type information can be present and finally it is possible to ''rename'' each of the constructs upon import. For types one needs also to use the keyword <code>struct</code> if one wish to get access to the ''internal structure'' of a particular type.		* '''Importing''': It is possible to import definitions that has been exported from other modules. This is done in an ''imports section'' that is started off with the keyword <code>imports</code> and followed by a sequence of imports from different modules. Each of these module imports are started with the keyword <code>from</code> followed by the name of the module and a module signature. The ''module signature'' can either simply be the keyword <code>all</code> indicating the import of all definitions exported from that module, or it can be a sequence of import signatures. The import signatures are specific for types, values, functions and operations and each of these are started with the corresponding keyword. In addition these import signatures name the constructs that there is a desire to get access to. In addition optional type information can be present and finally it is possible to ''rename'' each of the constructs upon import. For types one needs also to use the keyword <code>struct</code> if one wish to get access to the ''internal structure'' of a particular type.
Line 213:		Line 213:

	====Structuring in VDM++====		====Structuring in VDM++====
	In VDM++ structuring are done using classes and multiple inheritance. The key concepts are:		In VDM++ structuring are done using classes and [[multiple inheritance]]. The key concepts are:
	* '''Class''': Each class is syntactically started with the keyword <code>class</code> followed by the name of the class. At the end of a class the keyword <code>end</code> is written followed again by the name of the class.		* '''Class''': Each class is syntactically started with the keyword <code>class</code> followed by the name of the class. At the end of a class the keyword <code>end</code> is written followed again by the name of the class.
	* '''Inheritance''': In case a class inherits constructs from other classes the class name in the class heading can be followed by the keywords <code>is subclass of</code> followed by a comma-separated list of names of superclasses.		* '''Inheritance''': In case a class inherits constructs from other classes the class name in the class heading can be followed by the keywords <code>is subclass of</code> followed by a comma-separated list of names of superclasses.
Line 240:		Line 240:
	The precondition and postcondition together form a ''contract'' that to be satisfied by any program claiming to implement the function. The precondition records the assumptions under which the function guarantees to return a result satisfying the postcondition. If a function is called on inputs that do not satisfy its precondition, the outcome is undefined (indeed, termination is not even guaranteed).		The precondition and postcondition together form a ''contract'' that to be satisfied by any program claiming to implement the function. The precondition records the assumptions under which the function guarantees to return a result satisfying the postcondition. If a function is called on inputs that do not satisfy its precondition, the outcome is undefined (indeed, termination is not even guaranteed).

	VDM-SL also supports the definition of executable functions in the manner of a functional programming language. In an ''explicit'' function definition, the result is defined by means of an expression over the inputs. For example, a function that produces a list of the squares of a list of numbers might be defined as follows:		VDM-SL also supports the definition of executable functions in the manner of a [[functional programming]] language. In an ''explicit'' function definition, the result is defined by means of an expression over the inputs. For example, a function that produces a list of the squares of a list of numbers might be defined as follows:
	<syntaxhighlight lang="rsl">		<syntaxhighlight lang="rsl">
	SqList: seq of nat -> seq of nat		SqList: seq of nat -> seq of nat
Line 270:		Line 270:

	===State-based modelling===		===State-based modelling===
	In VDM-SL, functions do not have side-effects such as changing the state of a persistent global variable. This is a useful ability in many programming languages, so a similar concept exists; instead of functions, ''operations'' are used to change '''state variables''' (also known as ''globals'').		In VDM-SL, functions do not have side-effects such as changing the state of a persistent [[global variable]]. This is a useful ability in many programming languages, so a similar concept exists; instead of functions, ''operations'' are used to change '''state variables''' (also known as ''globals'').

	For example, if we have a state consisting of a single variable <code>someStateRegister : nat</code>, we could define this in VDM-SL as:		For example, if we have a state consisting of a single variable <code>someStateRegister : nat</code>, we could define this in VDM-SL as:
Line 403:		Line 403:
	==Tool support==		==Tool support==
	A number of different tools support VDM:		A number of different tools support VDM:
	* [http://www.vdmtools.jp/en VDMTools] was the leading commercial tools for VDM and VDM++, owned, marketed, maintained and developed by [http://www.csk.com CSK Systems], building on earlier versions developed by the Danish Company IFAD. The [http://www.vdmtools.jp/en/modules/tinyd2/index.php?id=2 manuals] and a practical [http://www.vdmportal.org/twiki/pub/Main/WebHome/tutorial1.pdf tutorial] are available. All licenses are available, free of charge, for the full version of the tool. The full version includes automatic code generation for Java and C++, dynamic link library and CORBA support.		* [http://www.vdmtools.jp/en VDMTools] was the leading commercial tools for VDM and VDM++, owned, marketed, maintained and developed by [http://www.csk.com CSK Systems], building on earlier versions developed by the Danish Company IFAD. The [http://www.vdmtools.jp/en/modules/tinyd2/index.php?id=2 manuals] and a practical [http://www.vdmportal.org/twiki/pub/Main/WebHome/tutorial1.pdf tutorial] {{Webarchive\|url=https://web.archive.org/web/20081119145552/http://www.vdmportal.org/twiki/pub/Main/WebHome/tutorial1.pdf \|date=19 November 2008 }} are available. All licenses are available, free of charge, for the full version of the tool. The full version includes automatic code generation for Java and C++, dynamic link library and CORBA support.
	* [http://www.overturetool.org/ Overture] is a community-based open source initiative aimed at providing freely available tool support for all VDM dialects (VDM-SL, VDM++ and VDM-RT) originally on top of the Eclipse platform but subsequently on top of the Visual Studio Code platform. Its aim is to develop a framework for interoperable tools that will be useful for industrial application, research and education.		* [http://www.overturetool.org/ Overture] is a community-based open source initiative aimed at providing freely available tool support for all VDM dialects (VDM-SL, VDM++ and VDM-RT) originally on top of the Eclipse platform but subsequently on top of the Visual Studio Code platform. Its aim is to develop a framework for interoperable tools that will be useful for industrial application, research and education.
	* [https://github.com/peterwvj/vdm-mode vdm-mode] is a collection of Emacs packages for writing VDM specifications using VDM-SL, VDM++ and VDM-RT. It supports syntax highlighting and editing, on-the-fly syntax checking, template completion and interpreter support.		* [https://github.com/peterwvj/vdm-mode vdm-mode] is a collection of Emacs packages for writing VDM specifications using VDM-SL, VDM++ and VDM-RT. It supports syntax highlighting and editing, on-the-fly syntax checking, template completion and interpreter support.
	* [http://www.adelard.com/web/hnav/services/SoftwareTools/SpecBox/index.html SpecBox]: from Adelard provides syntax checking, some simple semantic checking, and generation of a LaTeX file enabling specifications to be printed in mathematical notation. This tool is freely available but it is not being further maintained.		* [http://www.adelard.com/web/hnav/services/SoftwareTools/SpecBox/index.html SpecBox] {{Webarchive\|url=https://web.archive.org/web/20110707083149/http://www.adelard.com/web/hnav/services/SoftwareTools/SpecBox/index.html \|date=7 July 2011 }}: from Adelard provides syntax checking, some simple semantic checking, and generation of a LaTeX file enabling specifications to be printed in mathematical notation. This tool is freely available but it is not being further maintained.
	* [[LaTeX]] and LaTeX2e macros are available to support the presentation of VDM models in the ISO Standard Language's mathematical syntax. They have been developed and are maintained by the National Physical Laboratory in the UK. [http://ftp.npl.co.uk/pub/latex/macros/vdm-sl/README Documentation] and the [http://ftp.npl.co.uk/pub/latex/macros/vdm-sl/ macros] are available online.		* [[LaTeX]] and LaTeX2e macros are available to support the presentation of VDM models in the ISO Standard Language's mathematical syntax. They have been developed and are maintained by the National Physical Laboratory in the UK. [http://ftp.npl.co.uk/pub/latex/macros/vdm-sl/README Documentation] and the [http://ftp.npl.co.uk/pub/latex/macros/vdm-sl/ macros] are available online.

Line 509:		Line 509:
	* {{Cite book\| last = O'Regan \| first = Gerard \| title = Mathematical Approaches to Software Quality \| publisher = Springer \| year = 2006 \| location = London \| isbn = 978-1-84628-242-3 }}		* {{Cite book\| last = O'Regan \| first = Gerard \| title = Mathematical Approaches to Software Quality \| publisher = Springer \| year = 2006 \| location = London \| 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}}		* {{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}}
	* [[John Fitzgerald (computer scientist)\|Fitzgerald, J.S.]] and Larsen, P.G., ''Modelling Systems: Practical Tools and Techniques in Software Engineering''. [[Cambridge University Press]], 1998 {{ISBN\|0-521-62348-0}} (Japanese Edition pub. [[Iwanami Shoten]] 2003 {{ISBN\|4-00-005609-3}}).<ref>[http://www.csr.ncl.ac.uk/modelling-book/ ''Modelling Systems: Practical Tools and Techniques in Software Engineering'']</ref>		* [[John Fitzgerald (computer scientist)\|Fitzgerald, J.S.]] and Larsen, P.G., ''Modelling Systems: Practical Tools and Techniques in Software Engineering''. [[Cambridge University Press]], 1998 {{ISBN\|0-521-62348-0}} (Japanese Edition pub. [[Iwanami Shoten]] 2003 {{ISBN\|4-00-005609-3}}).<ref>{{Cite web \|url=http://www.csr.ncl.ac.uk/modelling-book/ \|title=''Modelling Systems: Practical Tools and Techniques in Software Engineering'' \|access-date=8 September 2007 \|archive-date=17 May 2012 \|archive-url=https://web.archive.org/web/20120517032626/http://www.csr.ncl.ac.uk/modelling-book/ \|url-status=dead }}</ref>
	* [[John Fitzgerald (computer scientist)\|Fitzgerald, J.S.]], Larsen, P.G., Mukherjee, P., Plat, N. and Verhoef, M., ''Validated Designs for Object-oriented Systems''. [[Springer Verlag]] 2005. {{ISBN\|1-85233-881-4}}. Supporting web site [http://www.vdmbook.com] includes examples and free tool support.<ref>[http://www.vdmbook.com/ ''Validated Designs for Object-oriented Systems'']</ref>		* [[John Fitzgerald (computer scientist)\|Fitzgerald, J.S.]], Larsen, P.G., Mukherjee, P., Plat, N. and Verhoef, M., ''Validated Designs for Object-oriented Systems''. [[Springer Verlag]] 2005. {{ISBN\|1-85233-881-4}}. Supporting web site [http://www.vdmbook.com] includes examples and free tool support.<ref>[http://www.vdmbook.com/ ''Validated Designs for Object-oriented Systems'']</ref>
	* [[Cliff Jones (computer scientist)\|Jones, C.B.]], ''Systematic Software Development using VDM'', [[Prentice Hall]] 1990. {{ISBN\|0-13-880733-7}}. Also available on-line and free of charge: http://www.csr.ncl.ac.uk/vdm/ssdvdm.pdf.zip		* [[Cliff Jones (computer scientist)\|Jones, C.B.]], ''Systematic Software Development using VDM'', [[Prentice Hall]] 1990. {{ISBN\|0-13-880733-7}}. Also available on-line and free of charge: http://www.csr.ncl.ac.uk/vdm/ssdvdm.pdf.zip {{Webarchive\|url=https://web.archive.org/web/20110717084413/http://www.csr.ncl.ac.uk/vdm/ssdvdm.pdf.zip \|date=17 July 2011 }}
	* [[Dines Bjørner\|Bjørner, D.]] and [[Cliff Jones (computer scientist)\|Jones, C.B.]], ''Formal Specification and Software Development'' [[Prentice Hall]] International, 1982. {{ISBN\|0-13-880733-7}}		* [[Dines Bjørner\|Bjørner, D.]] and [[Cliff Jones (computer scientist)\|Jones, C.B.]], ''Formal Specification and Software Development'' [[Prentice Hall]] International, 1982. {{ISBN\|0-13-880733-7}}
	* J. Dawes, ''The VDM-SL Reference Guide'', [[Pitman (publisher)\|Pitman]] 1991. {{ISBN\|0-273-03151-1}}		* J. Dawes, ''The VDM-SL Reference Guide'', [[Pitman (publisher)\|Pitman]] 1991. {{ISBN\|0-273-03151-1}}
Line 524:		Line 524:
	==External links==		==External links==
	* [https://web.archive.org/web/20080828013815/http://www.vdmportal.org/ Information on VDM and VDM++ (archived copy at archive.org)]		* [https://web.archive.org/web/20080828013815/http://www.vdmportal.org/ Information on VDM and VDM++ (archived copy at archive.org)]
	* [http://hopl.murdoch.edu.au/showlanguage2.prx?exp=598 Vienna Definition Language (VDL)]		* [http://hopl.murdoch.edu.au/showlanguage2.prx?exp=598 Vienna Definition Language (VDL)] {{Webarchive\|url=https://web.archive.org/web/20090519011520/http://hopl.murdoch.edu.au/showlanguage2.prx?exp=598 \|date=19 May 2009 }}
	* [http://www.compass-research.eu/approach.html COMPASS Modelling Language] {{Webarchive\|url=https://web.archive.org/web/20200219205126/http://www.compass-research.eu/approach.html \|date=19 February 2020 }} (CML), a combination of VDM-SL with [[Communicating sequential processes\|CSP]], based on [[Unifying Theories of Programming]], developed for modelling [[System of systems\|Systems of Systems]] (SoS)		* [http://www.compass-research.eu/approach.html COMPASS Modelling Language] {{Webarchive\|url=https://web.archive.org/web/20200219205126/http://www.compass-research.eu/approach.html \|date=19 February 2020 }} (CML), a combination of VDM-SL with [[Communicating sequential processes\|CSP]], based on [[Unifying Theories of Programming]], developed for modelling [[System of systems\|Systems of Systems]] (SoS)

Vienna Development Method - Revision history

imported>Thekittyburger: /* growthexperiments-addlink-summary-summary:1|2|0 */

imported>Cedar101: replace lang="prolog" with lang="rsl" (another formal specification language)