Part III: The Facet Language

Chapter List

Part Overview

The basic unit of Rosetta specification is the facet. Each facet describes one domain-specific system model. Each facet extends a domain, called its type, that provides a domain-specific modeling vocabulary and semantic basis. Facets are parameterized and may define local items. Facet properties are defined by a collection of terms that are either Boolean or facet valued. Boolean terms define properties directly while facet terms define structure by instantiating and interconnecting facets.

Part III describes the Rosetta the facet language used to encapsulate items in structures that define system models. The facet language is used to define and assign domains to facets, define packages containing specifications and libraries where they are stored, and components that encapsulate functional requirements, usage assumptions and correctness conditions.

After completing the chapters in Part III, you will understand how to declare facets, compose facets into structural specifications, define and use components, define libraries, and group specifications together into packages.

Overview

Thus far, our exploration of Rosetta has concentrated on the Rosetta expression language used to define Rosetta items and state mathematical properties over those items. Although the expression language is useful in its own right, it does not provide a mechanism for defining models where multiple properties hold simultaneously over multiple system observers. Nor does it provide mechanisms for modeling how properties change over time.

We look now at the facet language for defining the...