Concrete Syntax of VDM-SL Lite

Type Definitions

type definition = identifier , `=' , type , [ invariant ] | identifier , `::' , field list , [ invariant ]

type = bracketed type | basic type | quote type | union type | tuple type | optional type | set type | seq type | map type | function type | type name

bracketed type = `(' , type , `)'

basic type = `bool' | `nat' | `nat1' | `int' | `real' | `char' | `token'

quote type = quote literal

union type = type , `|' , type , { `|' , type }

tuple type = type , `*' , type , { `*' , type }

optional type = `[' , type , `]'

set type = `set of' , type

seq type = `seq of' , type

map type = `map' , type , `to' , type

function type = discretionary type , `->' , type

discretionary type = type | `(' , `)'

type name = name

field list = { field }

field = [ identifier , `:'] , type

State Definition

invariant = `inv' , invariant initial function

initialization = `init' , invariant initial function

invariant initial function = pattern , `==' , expression

Value Definitions

value definition = name , [ `:' , type ] , `=' , expression

Function Definitions

function definition = explicit function definition | implicit function definition

explicit function definition = identifier , `:' , function type , identifier , parameters , `==' , expression , [ `pre' , expression ] ,

implicit function definition = identifier , parameter types , identifier type pair , [ `pre' , expression ] , `post' , expression

identifier type pair = identifier , `:' , type

parameter types = `(' , [ pattern type pair list ] , `)'

pattern type pair list = pattern list , `:' , type , { `,' , pattern list , `:' , type }

parameters = `(' , [ pattern list ] , `)'

Operation Definitions

operation definition = identifier , parameter types , [ identifier type pair ] , [ externals ] , [ `pre' , expression ] , `post' , expression

operation type = discretionary type , `==>' , discretionary type

externals = `ext' , var information , { var information }

var information = mode , name list , [ `:' , type ]

mode = `rd' | `wr'

Expressions

expression = bracketed expression | let expression | let be expression | if expression | cases expression | unary expression | binary expression | quantified expression | set enumeration | set comprehension | set range expression | sequence enumeration | sequence comprehension | subsequence | map enumeration | map comprehension | tuple constructor | record constructor | apply | field select | is expression | name | old name | symbolic literal

Bracketed Expressions

Local Binding Expressions

let be expression = `let' , bind , [ `be' , `st' , expression ] , `in' , expression

Conditional Expressions

elseif expression = `elseif' , expression , `then' , expression

cases expression = `cases' , expression , `:' , cases expression alternatives , [ `,' , others expression ] , `end'

cases expression alternatives = cases expression alternative , { `,' , cases expression alternative }

cases expression alternative = pattern list , `->' , expression

others expression = `others' , `->' , expression

Unary Expressions

unary operator = `+' | `-' | `abs' | `not' | `card' | `power' | `dunion' | `dinter' | `hd' | `tl' | `len' | `elems' | `inds' | `conc' | `dom' | `rng' | `merge'

Binary Expressions

binary operator = `+' | `-' | `*' | `/' | `div' | `mod' | `<' | `<=' | `>' | `>=' | `=' | `<>' | `or' | `and' | `=>' | `<=>' | `in set' | `not in set' | `subset' | `union' | `\' | `inter' | `^' | `++' | `munion' | `<:' | `<-:' | `:>' | `:->'

Quantified Expressions

all expression = `forall' , bind list , `&' , expression

exists expression = `exists' , bind list , `&' , expression

exists unique expression = `exists1' , bind , `&' , expression

Set Expressions

set comprehension = `{' , expression , `|' , bind list , [ `&' , expression ] , `}'

set range expression = `{' , expression , `,' , `...' , `,' , expression , `}'

Sequence Expressions

sequence comprehension = `[' , expression , `|' , set bind , [ `&' , expression ] , `]'

subsequence = expression , `(' , expression , `,' , `...' , `,' , expression , `)'

Map Expressions

maplet = expression , `|->' , expression

map comprehension = `{' , maplet , `|' , bind list , [ `&' , expression ] , `}'

Tuple Constructor Expression

Record Expressions

Apply Expressions

field select = expression , `.' , identifier

Is Expressions

is basic type = `is_' , ( `bool' | `nat' | `nat1' | `int' | `rat' | `real' | `char' | `token')

Names

identifier = ( plain letter ) , { ( plain letter ) | digit | `'' | `_'}

name list = name , { `,' , name }

old name = identifier , `~'

Literals

numeral = digit , { digit }

numeric literal = numeral , [ `.' , digit , { digit }] , [ exponent ]

exponent = ( `E' | `e') , [ `+' | `-'] , numeral

boolean literal = `true' | `false'

nil literal = `nil'

character literal = `'' , character - newline , `''

character = plain letter | digit | delimiter character | other character | separator

separator = newline | white space

text literal = `"' , { `""' | character - ( `"' | newline )} , `"'

quote literal = distinguished letter , { `_' | distinguished letter | digit }

Patterns

pattern identifier = identifier | `-'

match value = `(' , expression , `)' | symbolic literal

set enum pattern = `{' , [ pattern list ] , `}'

set union pattern = pattern , `union' , pattern

seq enum pattern = `[' , [ pattern list ] , `]'

seq conc pattern = pattern , `^' , pattern

tuple pattern = `mk_' , `(' , pattern , `,' , pattern list , `)'

record pattern = `mk_' , name , `(' , [ pattern list ] , `)'

pattern list = pattern , { `,' , pattern }

Bindings

bind = set bind | type bind

set bind = pattern , `in set' , expression

type bind = pattern , `:' , type

bind list = multiple bind , { `,' , multiple bind }

multiple bind = multiple set bind | multiple type bind

multiple set bind = pattern list , `in set' , expression

multiple type bind = pattern list , `:' , type

Character set

a  b  c  d  e  f  g  h  i  j  k  l  m
n  o  p  q  r  s  t  u  v  w  x  y  z
A  B  C  D  E  F  G  H  I  J  K  L  M
N  O  P  Q  R  S  T  U  V  W  X  Y  Z

a  b  c  d  e  f  g  h  i  j  k  l  m
n  o  p  q  r  s  t  u  v  w  x  y  z

,   :   ;   =   (   )   |   -   [   ]
{   }   +   /   <   >   <=  >=  <>  .
*   ->  +> ==>  ||  =>  <=> |->  <: :>

-   `   '   "   @   ~

0  1  2  3  4  5  6  7  8  9

The distinguished letters use the corresponding capital and lower-case letters where the whole quote literal is preceded by "<" and followed by ">" (note that quote literals also can use underscores).

newline

This has no graphical form

white space

This has no graphical form