A strongly typed language for specifying programs

A language for specifying and annotating programs is presented. The language is intended to be used in connection with a strongly typed programming language. It provides a framework for the definition of specification concepts and the specification of programs by means of assertions and annotations. The language includes facilities for defining concepts axiomatically and to group definitions of related concepts and derived properties (lemmas) in theories. All entities in the language are required to be strongly typed; however, the language provides a very flexible type system which includes polymorphic (or generic) types. The paper presents a type checking algorithm for the language and discusses the relationship between specification language and programming language.