Overview

The Rosetta expression language is used to define properties involving Rosetta items. The simplest Rosetta expression is an atomic expression consisting of a literal or an item name and forms the leaves of the expression tree. Function and operator applications define operations over other expressions by instantiating function values with actual parameters. The if and case expressions define selection operations using boolean conditions and set membership, respectively. The let expression defines local variables over expressions. Because all expression types other than atomic expressions are defined recursively over expressions, compound expressions are formed by nesting expressions of all types.

All Rosetta expressions from atomic to compound have associated types. Determining types is instrumental to analyzing specifications for type safety, a critical aspect of system correctness. Due to the richness of the Rosetta type system, typing and type checking are particularly critical to successful design activities. To determine the type of an expression, Rosetta uses a combination of declared and asserted type information with rules for each expression type. The types of atomic expressions can be learned from their declarations. Similarly, the types of function and operator applications can be learned from their declarations and parameter values. Special rules exist for inferring the types of if, case, and let expressions from their sub-expressions.

3.1 Atomic Expressions

An atomic expression is the simplest expression consisting of a value or an item label. Such expressions are called atomic because they cannot be...