Chapter 4. Defining Units

Table of Contents
Conceptual Model
Realization via the File System
Unit Definitions Are Managed Outside of Specware

Conceptual Model

A unit definition consists of a unit identifier and a unit term. The identifier identifies the unit and the term defines how the unit is constructed.

An application developed with Specware consists of a set of unit definitions, some of which may come from libraries. Units have unique identifiers within the application.

Unit Identifiers

A unit identifier is a finite, non-empty sequence of word symbols (word symbols are defined in the Metaslang grammar). The sequence of word symbols is essentially a "path" in a tree: the units comprising an application are organized in a tree.

This provides a convenient and mundane way to organize the units comprising an application. Libraries are subtrees of the whole tree. Parallel development of different parts of an application can be carried out in different subtrees that can be later put together without risk of naming clashes.

Unit Terms

A unit term is text written in the Metaslang language. Metaslang features various ways to construct specs, morphisms, and all the other kinds of units. For instance, it is possible to construct a spec by explicitly listing its sorts, ops, and axioms. It is also possible to construct a spec by applying the colimit operation to a diagram of specs and morphisms.

A unit term may reference other units. For instance, a spec constructed by extending another one references the spec being extended.