The Facet Language
The basic unit of Rosetta speciﬁcation is the facet. Each facet describes one
domain-speciﬁc system model. Each facet extends a domain, called its type,
that provides a domain-speciﬁc modeling vocabulary and semantic basis.
Facets are parameterized and may deﬁne local items. Facet properties are
deﬁned by a collection of terms that are either Boolean or facet valued.
Boolean terms deﬁne properties directly while facet terms deﬁne structure
by instantiating and interconnecting facets.
Part III describes the Rosetta the facet language used to encapsulate items
in structures that deﬁne system models. The facet language is used to deﬁne
and assign domains to facets, deﬁne packages containing speciﬁcations 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 speciﬁcations, deﬁne and
use components, deﬁne libraries, and group speciﬁcations together into
This Page Intentionally Left Blank