The conceptual model just described is realized by means of the file system of the underlying operating system. The file system has essentially a tree structure. The tree of units comprising a Specware application is mapped to subtrees of the file system; the word symbols comprising a path are mapped to file and directory names.
Future versions of Specware will have a more sophisticated UI that will realize the conceptual model directly. Users will graphically see the units organized in a tree and they will be able to add, remove, move, and edit them. The mapping to the file system may even be made totally transparent to the user.
The mapping of the conceptual unit tree to the file system is defined by the environment variable SWPATH. Similarly to the PATH environment variable in operating systems, SWPATH is a string consisting of a semicolon-separated list of absolute directory paths in the file system. See the Section called Inspecting and Setting SWPATH in Chapter 5 for information on how to inspect and set SWPATH.
Roughly speaking, the unit tree consists of all the units defined in .sw files under the directories listed in SWPATH. The identifier of each unit is its path from the directory in SWPATH under which the file defining the unit is: if the unit is under directory dir, its identifier is its absolute path in the file system "minus" the dir prefix. This approximate statement is made precise and illustrated by examples below.
The simplest way to define a unit is to write its term into a .sw file in the subtree of one of the directories in SWPATH. The identifier of the unit is the name of the file, without .sw, prefixed by the path from the directory in SWPATH to the file.
For example, suppose that SWPATH includes the directory c:\users\me\specware. The user creates a file named A.sw immediately under the directory c:\users\me\specware\one\two, containing the following text:
spec
sort X
endspec |
The absolute path of the file in the file system is c:\users\me\specware\one\two\A.sw. The unit is a spec containing just a sort X. The identifier of the unit is /one/two/A. Note that the path components are separated by "/" (forward slash), even though the underlying file system uses "\" (backward slash). Unit identifier are sequences of word symbols separated by "/", regardless of the underlying operating system.
It is also possible to put multiple units inside a .sw file. The file must be in the subtree of one of the directories in SWPATH. Instead of just containing a unit term, the file contains one or more unit definitions. A unit definition consists of a word symbol, "=" (equal), and a unit term.
This case works almost exactly as if the file were replaced by a directory with the same name (without .sw) containing one .sw file for every unit defined therein. Each such file has the word symbol of the unit as name (plus .sw) and the term of the unit as content.
The only difference between the case of multiple units per file and the almost equivalent case where the file is replaced by a directory containing single-unit files, is that in the former case the last separator is not "/" but "#" (sharp). (This is reminiscent of the URI syntax, where subparts of a document are referred to using "#".)
Suppose, as in the previous example, that SWPATH includes the directory c:\users\me\specware. The user creates a file named three.sw immediately under the directory c:\users\me\specware\one\two, containing the following text:
B = spec
sort Y
endspec
C = spec
sort Z
endspec |
This file defines two specs, one containing just a sort Y, the other containing just a sort Z. The identifier of the first spec is /one/two/three#B, the identifier of the second spec is one/two/three#C.
As a particular instance of the case of multiple units per file, it is possible to have just one unit definition in the file. This is different from just having a unit term in a file. If the file contains a unit definition, then the word symbol at the left of "=" is part of the unit's identifier, together with "#" and the file path (relative to the directory in SWPATH). If instead the file contains a unit term, then the identifier of the unit is the file path (relative to the directory in SWPATH), without any "#" and additional word symbol.
Despite the possibility of having one unit definition in a file, in this manual we use the term "multiple-unit file" to denote a file that contains one or more unit definitions. The term "single-unit file" is instead used to denote a file that only contains a unit term.