22 Chapter 2 Items, Values, Types, and Declarations
real >= integer // real is a supertype of integer
real > integer // real is a proper supertype of integer
Rosetta item values must always be taken from their associated types. This
fact is the heart of Rosetta type and constraint checking. As we will see, using a
sophisticated and ﬂexible type system allows assertion and veriﬁcation of complex
properties in a compact and readable form.
2.2 Item Declarations and Type Assertions
Item declarations occur in declar ative regions, parameter lists, functions, and
let forms where new variables and constants are required. Each item declara-
tion creates a new item with a label and must be annotated with a type assertion.
A Rosetta type assertion uses the assertion operator “
::” to associate a ty pe with
an item. Whenever we use the notation
x::T, we are asserting that the value asso-
ciated with the item labeled
x isamemberofthetypeT. All declarations must
include a type assertion, but t ype assertions may be used to indicate types any-
where in a Rosetta speciﬁcation. Thus, type assertions are used to assign types to
new items and to specify types for items in expressions.
2.2.1 Item Declarations
When the type assertion
x::T appears in a declarative region such as a facet’s local
let clause or parameter list, it represents an item declaration or
simply a declaration. A declaration of this form adds a new item labeled
x to the
current lexical context with the assertion that
Each declaration achieves three results: (i) it creates and labels a new item in
the current scope; (ii) it assigns a type to the item, deﬁning potential values for
the item; and; (iii) it may bind a value to the item. If a declaration does not bind
a value to an item, the item is considered a variable. If a declaration does bind a
value to an item, the item is considered a constant.
An example of a Rosetta declaration that deﬁnes an item named
mean :: real is 13.5;
In this declar ation, mean is the label of the new item and provides a name used to
refer to the item. The type assertion operator assigns a type to the newly declared
item. In this example, the type speciﬁed is
real, requiring that any value associ-
ated with the item must be a real number. The type speciﬁcation is followed by an
optional value constraint speciﬁed by the
is clause that binds the item’s value to
a constant. In this example, the value of mean is equal to the constant value
The value speciﬁed by the
is clause is not an initialization value. The is clause
asserts that the declared item’s value must always be equal to the speciﬁed value.
Thus, the value of
mean will always be 13.5 in the scope of this declaration.