A.2 ValuesA Specification LanguageA.1 Types

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

A.2 ValuesA Specification LanguageA.1 Types