Natural number, which is an element of the predefined data sort Pos.Ĭonsider the following, incomplete data specification (available for download We shall use lists to represent stacks of discs, such that the head of the listĬorresponds with the top of the stack. The mCRL2 language supports more operations on lists, but they are not used in Not further reduce the terms head() and tail(). Note that the head and tail of an empty list are undefined, so that mCRL2 will tail: return a list without its first element, e.g.head: return the first element of a list, e.g.snoc cons |>: insert an element at the front of a list, e.g.List with single element 1 and the list with elements 2, 3 and 5, respectively.įurthermore, the following operations on lists are provided: Lists can be explicitly enumerated, so that, ,Īnd are all valid list expressions, representing the empty list, the For example, a list l of natural numbers is declared by This type is determined by the list’s type declaration, whichĬonsists of the word List followed by the type of its elements between The list data structure is predefined in mCRL2. Represent a peg and we shall use a list to represent the contents of a peg. For this, we shall specify a Peg process to Over the next exercises we gradually construct an mCRL2 specification of the
0 Comments
Leave a Reply. |