Specware Project

The Specware system consists of a formal specification language, Metaslang, and a variety of support tools. A Metaslang specification is comprised of types, operators, axioms expressed in higher-order logic, and definitions. Specifications are structured using importation and composition by colimit, a category-theoretic universal construction. Metaslang supports higher-order operations and polymorphic types with predicate subtypes.

Specware provides a standard library, specifying basic data types with verified proofs, and executable refinements. It also has built up a library of over 40 transformations for generating refinements.

Specware is self-specified. It has backends to generate executable CommonLisp, C, Java, or Haskell code. It has a translator from Metaslang to Isabelle/HOL that is used to discharge proof obligations. More information on Specware is available at specware.org