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 flexible type system allows assertion and verification 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 specification. 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
declarations, a
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
x isamemberoftypeT.
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, defining 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 defines an item named
mean is:
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 specified is
real, requiring that any value associ-
ated with the item must be a real number. The type specification is followed by an
optional value constraint specified 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
13.5.
The value specified 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 specified value.
Thus, the value of
mean will always be 13.5 in the scope of this declaration.

Get System Level Design with Rosetta now with O’Reilly online learning.

O’Reilly members experience live online training, plus books, videos, and digital content from 200+ publishers.