Unit definitions are processed by Specware. The user instructs Specware to process units by supplying certain commands. Specware has access, via the Lisp runtime environment, to the underlying file system, so it can access the .sw files that define units. The environment variable SWPATH determines which .sw files are accessed by Specware to find unit definitions.
Processing a unit causes the recursive processing of the units referenced in that unit's term. For instance, if a spec A extends a spec B which in turns extends a spec C, then when A is processed, B and C are also processed. There must be no circularities in the chain of unit dependencies.
Processing causes progress and/or error messages to be displayed in the XEmacs buffer containing the Lisp shell (which is also where the user supplies commands to Specware). Progress messages inform the user that units were processed without error. Error messages provide information on the cause of errors, so that the user can fix them by editing the unit definitions. When an error occurs in the definition of some unit, Specware displays the .sw file containing the unit term in a separate XEmacs buffer, with the cursor positioned at the point containing the erroneous text.
The processing of certain kinds of units also results in the creation of new files as an additional side effect. For instance, Lisp programs are a kind of unit, constructed by the generate operation of Metaslang. A side effect of processing one such unit is that the resulting code is written into a .lisp file.
When Specware processes a unit, it saves the processing results into an internal cache, associating the results with the unit's identifier. By using this cache, Specware avoids unnecessary re-computations: it only re-processes the units whose files have changed since the last time they were processed. From the point of view of the final result, this caching mechanism is completely transparent to the user. However, it improves the performance and response time of the system.