Constructor Terms

XASM provides the possibility to define and use constructor terms. The concept of constructor terms can be mapped to the ASM core language as follows: According to [16] each of the function names contained in the vocabulary V of an ASM may be marked as relational or static, or both. In addition, we allow static functions to be marked as constructive. Let $F_c$ be the set containing all functions in V marked as constructive, $F_c \subseteq V$. Let $f_c \in F_c$, arity of $f_c = n$, then the following conditions hold for all states A of the ASM:

(i)

$\forall t_1,\ldots,t_n, \mbox Val_A(t_i)\neq\undef, 1\leq i\leq n \bullet\\ \hspace*{2mm}f_c(t_1,\ldots,t_n) \neq \undef$

(ii)

$\begin{array}[t]{@{}l} \forall g_c\in F_c, \mbox{arity of $g_c$ is $m$};   t_1... ...pace*{2mm}\wedge \mbox Val_A(t_i) = \mbox Val_A(s_i), 1\leq i\leq n \end{array}$

where $\mbox Val_A(t)$ stands for the evaluation of term t in state A of the ASM. Informally speaking that means that each constructive function is (i) defined at all locations and that (ii) the content of each location is a unique element of the superuniverse w.r.t. the set of locations of all constructive functions. If $f_c \in F_c$, then $f_c$ is called a constructor, and the terms $f_c(t_1,\ldots,t_n)$ are called constructor terms. In XASM, the declaration of a constructor is part of the function declarations, for example

introduces the constructors nil, cons, empty, and children, where terms constructed using the latter two constructors are elements of the universe BinTree.

XASM also provides pattern matching functionality like it is used in many other languages. Syntactically, pattern matching terms are used as condition terms in conditionals, e. g.:

There are three kinds of pre-defined, commonly-used constructors in XASM: sets, sequences, and tuples. These constructors are specified using their usual representation: $\{x_1,\ldots,x_n\}$ for sets, $[x_1,\ldots,x_n]$ for sequence, and $(x_1,\ldots,x_n)$ for n-tuples. For sequences, the notation $[H\vert T]$ can be used in pattern matching terms for accessing head and tail of a sequence.