Download Specware 4.2 Language Manual

Chapter 2. Metaslang
Boolean
a
{center : XYpos, radius : Length}
(Nat | even)
{k : Key | present (db, k)}
(Nat * Nat)
Sample new-type-descriptors:
| Point XYpos | Line XYpos * XYpos
Nat / (fn (m, n) -> m rem 3 = n rem 3)
The meaning of the type-descriptor Boolean is the “inbuilt” type inhabited by the
two logical (truth) values true and false. The meaning of a parenthesized
type-descriptor (T ) is the same as that of the enclosed type-descriptor T.
The various other kinds of type-descriptors and new-type-descriptors not defined
here are described each in their following respective sections, with the exception of
local-type-variable, whose (lack of) meaning as a type-descriptor is described below.
Restriction. A local-type-variable may only be used as a type-descriptor if it occurs
in the scope of a formal-type-parameters or type-variable-binder in which it is
introduced.
Disambiguation. A single simple-name used as a type-descriptor is a
local-type-variable when it occurs in the scope of a formal-type-parameters or
type-variable-binder in which it is introduced, and then it identifies the textually most
recent introduction. Otherwise, the simple-name is a type-name.
A local-type-variable used as a type-descriptor has no meaning by itself, and where
relevant to the semantics is either “indexed away” (for parameterized types) or
“instantiated away” (when introduced in a formal-type-parameters or
type-variable-binder) before a meaning is ascribed to the construct in which it occurs.
Textually, it has a scope just like a plain local-variable.
2.5.1. Type-sums
type-sum ::= type-summand { type-summand }*
type-summand ::= | constructor [ slack-type-descriptor ]
constructor ::= simple-name
45