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]
		   { Domain-Equation } 
 *[0.5ex]
		   { Impl-Description } 
 *[2ex]
Domain-Equation::=Tree-Def|Other-Def 
 *[2ex]
Tree-Def::=Domain-Name    {
Selector-Name    Domain-Name } 
 *[2ex]
Other-Def::=Domain-Name    
 *[0.5ex]
		Set-Dom|Tuple-Dom| 
 *[0.5ex]
		Map-Dom|Union-Dom| 
 *[0.5ex]
		Optional-Dom|Token-Dom 
 *[2ex]
Set-Dom::=Domain-Name    
 *[2ex]
Tuple-Dom::=Domain-Name (   
|    ) 
 *[2ex]
Map-Dom::=Domain-Name   
Domain-Name 
 *[2ex]
Union-Dom::=[ Selector-Name    ] Domain-Name

 *[0.5ex]
				{    [ Selector-Name    ]
Domain-Name } 
 *[2ex]
Optional-Dom::=   Domain-Name
   } 
 *[2ex]
Token-Dom::=    
 [2ex]
Impl-Description::=Domain-Name   

 *[0.5ex]
				[ Implementation [    Parameter
   ] ] 
 *[0.5ex]
				{    Enrichment [   
Parameter    ]} 
 *[2ex]
Parameter::= 
 *[0.5ex]
		Param-Name [    Param-Value ]
[    Parameter ] 
 *[2ex]
Param-Value::=   String
   | Number |    | 
Name 
 [2ex]
Domain-Name::=Uppercase{ Cont-Char } 
 *[2ex]
Selector-Name::=  { Cont-Char
} 
 *[2ex]
String::={ Every-Char } 
 *[2ex]
Number::={ Digit } 
 *[2ex]
Name::=( Uppercase | Lowercase ) [ {
Cont-Char | Uppercase } ] 
 *[2ex]
Cont-Char::=
Lowercase | Digit |    
 *[3ex]

Einige Non-Terminalsymbole werden informal erläutert:

• Uppercase sind die Großbuchstaben
• Lowercase sind die Kleinbuchstaben
• Digit sind die Ziffern
• Every-Char sind alle Zeichen des Zeichensatzes
• Implementation ist der Name einer der für den zugrundeliegenden Typgenerator definierten Implementationen
• Enrichment  ist der generische Name einer der für den zugrundeliegenden Typgenerator definierten Operationen
• Param-Name ist der Name eines für die Implementation oder die Operation definierten Parameters