The user can construct specs by explicitly listing the types, ops, and axioms comprising the spec, possibly after importing one or more other specs. When a spec is processed, Specware typechecks all the expressions that appear in the spec. Typechecking means checking that the expressions are type-correct, according to the rules of the Metaslang language.
In general, only some of the ops and variables that appear in an expression have explicit type information. Typechecking also involves reconstructing the types of those ops and variables that lack explicit type information.
Typechecking is an integrated process that checks the type correctness of expressions while reconstructing the missing type information. This is done by deriving and solving type constraints from the expression. For instance, if it is known that an op f has type A -> B then the type of the variable x in the expression f(x) must be A, and the type of the whole expression must be B.
If the missing type information cannot be uniquely reconstructed and/or if certain constraints are violated, Specware signals an error, indicating the textual position of the problematic expression.
Since the Metaslang type system features subtypes defined by arbitrary predicates, it is in general undecidable whether an expression involving subtypes is type-correct or not. When Specware processes a spec, it assumes that the type constraints arising from subtypes are satisfied, thus making typechecking decidable.
The proof obligations associated with a spec, which are extracted via the Metaslang obligations operation, include conjectures derived from the type constraints arising from subtypes. If all of these conjectures can be proved (using a theorem prover) then all the expressions in the spec are type-correct.