Die Operationen der ADT VDM Tutor Der Aufruf von vdminfo

DSL-Syntax

 

Die Syntax einer DSL-Spezifikation wird in der Backus-Naur-Form definiert. Terminalsymbole sind umrahmt. Die geschweiften Klammern bedeuten das ein- bis n-malige Auftreten des geklammerten Ausdrucks.

 
DSL-Specification::= 
 *[0.5ex]
		 tex2html_wrap8457  { Domain-Equation } 
 *[0.5ex]
		 tex2html_wrap8459  { Impl-Description } 
 *[2ex]
Domain-Equation::=Tree-Def|Other-Def 
 *[2ex]
Tree-Def::=Domain-Name  tex2html_wrap8461  {
Selector-Name  tex2html_wrap8463  Domain-Name } 
 *[2ex]
Other-Def::=Domain-Name  tex2html_wrap8465  
 *[0.5ex]
		Set-Dom|Tuple-Dom| 
 *[0.5ex]
		Map-Dom|Union-Dom| 
 *[0.5ex]
		Optional-Dom|Token-Dom 
 *[2ex]
Set-Dom::=Domain-Name  tex2html_wrap8467  
 *[2ex]
Tuple-Dom::=Domain-Name (  tex2html_wrap8469 
|  tex2html_wrap8471  ) 
 *[2ex]
Map-Dom::=Domain-Name  tex2html_wrap8473 
Domain-Name 
 *[2ex]
Union-Dom::=[ Selector-Name  tex2html_wrap8463  ] Domain-Name

*[0.5ex] { tex2html_wrap8477 [ Selector-Name tex2html_wrap8463 ] Domain-Name } *[2ex] Optional-Dom::= tex2html_wrap8481 Domain-Name tex2html_wrap8483 } *[2ex] Token-Dom::= tex2html_wrap8485 [2ex] Impl-Description::=Domain-Name tex2html_wrap8465

*[0.5ex] [ Implementation [ tex2html_wrap8489 Parameter tex2html_wrap8491 ] ] *[0.5ex] { tex2html_wrap8471 Enrichment [ tex2html_wrap8489 Parameter tex2html_wrap8491 ]} *[2ex] Parameter::= *[0.5ex] Param-Name [  tex2html_wrap8465 Param-Value ] [  tex2html_wrap8501 Parameter ] *[2ex] Param-Value::= tex2html_wrap8503 String tex2html_wrap8503  | Number |  tex2html_wrap8507  |  Name [2ex] Domain-Name::=Uppercase{ Cont-Char } *[2ex] Selector-Name::= tex2html_wrap8509 { Cont-Char } *[2ex] String::={ Every-Char } *[2ex] Number::={ Digit } *[2ex] Name::=( Uppercase | Lowercase ) [ { Cont-Char | Uppercase } ] *[2ex] Cont-Char::= Lowercase | Digit |  tex2html_wrap8511 *[3ex]

Einige Non-Terminalsymbole werden informal erläutert:



VDM Class Library