have types that are determined statically. The type system is based on lifted sets where each type contains at least the bottom or undefined value. Any set can be used to define a type and any function that returns a set can be used to define a type former. Because type definitions can contain general Rosetta expressions, the type system is dependent. The facet language defines individual specifications and specification composition to define systems. Facets and components define system models from one engineering perspective. Each facet is written by extending a domain that provides vocabulary and semantics for the model. Facets are defined by declaring items and defining properties for those items. As such, Rosetta is a declarative language and constructs cannot be guaranteed to evaluate to a value, although some facets can be evaluated. Using the design abstractions provided by its domain, a facet describes requirements, behavior, constraints, or function of a system. Facets are heterogeneous and may be defined using any of the predefined or user defined domains. The Rosetta semantics denotes each facet to a coalgebra that defines its model-of-computation. Because Rosetta is reflective, facets can be composed and transformed to define complex systems. A common specification technique is to write facets for different aspects of a system and then compose those aspects using product and sum operations to define the complete system. The domain language defines specification domains otherwise known as specification types. The collection of domains forms a complete lattice ordered by homomorphism with the empty or null domain as its top element and the inconsistent or bottom domain as its bottom. There are three primary domain types. Units-of-semantics domains define basic units of specification. For example, the state_based domain defines the concept of state and next state without constraining the values or properties. Model-of-computation domains extend unit-of-semantics domains to define general computational models such as finite_state, continuous_time, discrete_time and frequency. Engineering domains extend model-of-computation domains to provide specification capabilities for specific engineering domains. Since its early days, Rosetta expanded to include design domains such as hydraulic and mechanical systems, networking systems, security and trust, and software defined radios. Further reading Rosetta was influenced heavily by the non-strict, purely functional language Haskell, the Larch family of specification languages, and Prototype Verification System (PVS). A book devoted to the language was published in November 2006. References External links http://www.rosetta-lang.org Formal specification languages IEEE standards