Language reference/Data syntax

From MCRL2



Syntax definition

Lexical syntax Data syntax Process syntax mu-calculus syntax PBES syntax

Contents

This page describes the concrete syntax of data specifications.

The syntax of sorts expressions, data expressions and data specifications is described.

Sort expressions

Sort expressions s:

s    ::=  b  |  s "->" s  |  "Bool"  |  "Pos"  |  "Nat"  |  "Int"  |  "Real"
       |  "struct" scs "|" ... "|" scs
       |  "List" "(" s ")"  |  "Set" "(" s ")"  |  "Bag" "(" s ")"
       |  "(" s ")"
scs  ::=  f  |  f "(" spj "," ... "," spj ")"
       |  f "?" f  |  f "(" spj "," ... "," spj ")" "?" f
spj  ::=  s  |  s "#" ... "#" s "->" s
       |  f ":" s  |  f ":" s "#" ... "#" s "->" s

Here scs and spj represent the constructor and projection functions of a structured sort. Furthermore, b stands for a sort name, and f for a function name, which are both identifiers.

The sort expression "b" represents a base sort and "s -> s" represents a function sort. Constant "Bool" represents the booleans, "Pos" the positive integers, "Nat" the non-negative integers, "Int" the integers, and "Real" the real numbers. Sort expressions starting with "struct" represent a structured sort, "List" a list sort, "Set" a set sort, and "Bag" a bag sort.

The binary operator "->" associates to the right. This can be overruled with the use of parentheses "(" and ")".

Data expressions

Data expressions d:

d    ::=  x  |  f  |  d "(" d "," ... "," d ")"  |  N  |  true  |  false  |  if
       |  "!" d  |  "-" d  |  "#" d  |  d ⊕ d
       |  "[]"  |  "[" d "," ... "," d "]"  |  "{}"  |  "{" d "," ... "," d "}"
       |  "{" d ":" d "," ... "," d ":" d "}"  |  "{ x ":" s "|" d "}"
       |  "forall" mvd "," ... "," mvd "." d  |  "exists" mvd "," ... "," mvd "." d
       |  "lambda" mvd "," ... "," mvd "." d  |  d "whr" x "=" d "," ... "," x "=" d "end"
       |  "(" d ")"
mvd  ::=  x "," ... "," x ":" s
⊕    ::=  "*"  |  "."  |  "/"  |  "div"  |  "mod"  |  "+"  |  "-"  |  "++"  |  "<|"  |  "|>" 
       |  "<"  |  "<=" |  ">=" |  ">"    |  "in"   |  "=="  |  "!="  |  "&&"  |  "||"  |  "=>"

Here mvd represents for a multiple data variable declaration, ⊕ for a binary operator, and s a sort expression. Furthermore, x stands for a data variable name, f for a function name, which are both identifiers; N stands for a number.

In the rules for data expressions, "x" represents a data variable, "f" a function, "d(d, ..., d)" a function application, and "N" a number. For the unary operators, "!" represents logical negation and set complement, "-" arithmetic negation, and "#" list size. For the binary operators, "*" represents multiplication and set/bag intersection, "." list element at, "/" division, "div" quotient of division, "mod" remainder of division, "+" addition and set/bag union, "-" subtraction and set/bag difference, "++" list concatenation, "<|" list snoc, "|>" list cons, "<" less-than and proper subset/subbag, "<=" less-than-or-equal and subset/subbag, ">=" greater-than-or-equal, ">" greater-than, "in" set/bag element test, "==" equality, "!=" inequality, "&&" conjunction, "||" disjunction and "=>" implication. Furthermore, "[]" represents the empty list, "[d,...,d]" list enumeration, "{}" the empty set/bag, "{d,...,d}" set enumeration, "{d:d,...,d:d}" bag enumeration and "{x:s|d}" set/bag comprehension. The rules involving "lambda", "forall" and "exists" represent for lambda abstraction, universal quantification and existential quantification respectively. Finally, the rule involving "whr" and "end" represents a where clause.

The unary operators have the highest priority, followed by the infix operators, followed by "lambda", "forall" and "exists", followed by "whr" "end". The descending order of precedence of the infix operators is: { "*", "." }, { "/", "div", "mod" }, { "+", "-" }, "++", "<|", "|>", { "<", "<=", ">=", ">", "in" }, { "==", "!=" }, { "&&", "||" }, "=>". Of these operators "*", ".", "/", "div", "mod", "+", "-", and "++" associate to the left and "==", "!=", "&&", "||" and "=>" associate to the right. These priorities can be overruled with the use of parentheses "(" and ")".

Data specifications

Data specifications data_spec:

data_spec  ::=  "sort" ( sd  ";" )+
             |  "cons" ( mfd ";" )+
             |  "map"  ( mfd ";" )+
             |  "var"  ( mvd ";" )+ "eqn" ( ed ";" )+
             |  "eqn"  ( ed  ";" )+
sd         ::=  b  |  b "=" s
mfd        ::=  f "," ... "," f ":" s
ed         ::=  d "=" d  |  c "->" d "=" d

Here, sd represents a sort declaration, mfd a multiple function declaration, ed a equation declaration, ad a action declaration, s a sort expression, and c and d data expressions, where c is of sort Bool. Furthermore, b stands for a sort name and f for a function name, which are both identifiers.

---

Lexical syntax

Process syntax