Chapter List

Part Overview

Before writing specifications, we must define a language to describe system properties. In Rosetta, system properties are describe with respect to items that represent units of specification. All items have types and values. By describing relationships between different items through their types and values, system properties can be defined.

Part II describes the Rosetta expression language used to declare items comprising a specification and define properties over those items. The expression language is used to declare items, assign types to items, and define properties among items. It is declarative, allowing specifiers to define properties. In contrast to writing programs that indirectly exhibit desired properties, declarative techniques allow the specifier to state specific properties directly. Furthermore, these properties can be incomplete and need not be executable.

After completing the chapters in Part II, you will understand how to declare items, use elemental and composite types, define and use functions and higher-order functions, and define new types.