Specware is a tool for building and manipulating a collection of related specifications. Specware can be considered:
a design tool, because it can represent and manipulate designs for complex systems, software or otherwise
a logic, because it can describe concepts in a formal language with rules of deduction
a programming language, because it can express programs and their properties
a database, because it can store and manipulate collections of concepts, facts, and relationships
Specifications are the primary units of information in Specware. A specification, or theory, describes a concept to some degree of detail. To add properties and extend definitions, you create new specifications that import or combine earlier specifications. Within a specification, you can reason about objects and their relationships. You declare sorts (data types) and operations (ops, functions), axioms that state properties of operations, and theorems that follow logically from axioms.
A morphism is a relationship between specifications that describes how the properties of one map to the properties of another. Morphisms describe both part-of and is-a relationships. You can propagate theorems from one specification to another using morphisms; for example, if the QEII is a ship, and ships cannot fly, then the QEII cannot fly.