A.1 Types
In this section, we describe the language's type expressions denoting
types i.e. domains of values. The type system is higher-order
i.e. it includes functions and does not make a fundamental difference between
functions and predicates (which are just functions whose result is a truth
value). Types are partially ordered by a subtype relationship such that
if T1 is a subtype of T2, any value of type T1 may occur
where a value of type T2 is expected. The specification language is
strongly typed; the system ensures type discipline for every
declaration by a combination of static checking and dynamic proving (see
Section A.3).
Wolfgang
Schreiner