A Specification LanguageA.2 ValuesA.3 Declarations

A.3 Declarations

In this section, we describe the language's declaration expressions denoting declarations each of which extends the environment by a mapping of an identifier to a type, value, or formula. When type checking a declaration, a type checking condition may be generated which is forwarded to a decision procedure for automatic proving. If the condition cannot be proved, a warning is issued, but the type checking condition is nevertheless assumed true. Thus the user must establish by a separate proof that the type checking condition is valid (any further proof might be unsound, otherwise).


Wolfgang Schreiner

A Specification LanguageA.2 ValuesA.3 Declarations