Overview

Rosetta's composite types define homogeneous collections of data. The composite type subsystem provides mechanisms for defining and manipulating three primary data containers, sets, multisets, and sequences. All composite types are homogeneous and are declared using type formers. Values from composite types are formed using associated value formers, whose syntax parallels type formers.

The set type defines unordered, homogeneous collections of unique items. A primary use for the set type is defining new types and subtypes. Additionally, sets provide excellent mechanisms for defining collections of items in abstract specifications. The multiset type defines an unordered, homogeneous collection of items, where multiple instances of an element are allowed. A primary use for multiset types is manipulating collections of values, where the number of values in a collection is significant. The sequence type defines indexed, homogeneous collections of data that resemble arrays and lists. A primary use for sequence types is ordering or structuring data collections. The sequence type has associated subtypes that represent strings and bit vectors as sequences of characters and bits, respectively.

5.1 Type Formers

All Rosetta composite types are defined using type formers. A type former is a function that takes one or more content types and generates a composite type with appropriate properties from them. All type formers have the following format:

• container ( T )

where container is the composite type and T is the type associated with items in the container. For example,...