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 window containing the Specware Shell. 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. If the Specware Shell is running under XEmacs, then, 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 of 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, C or Java programs are constructed by units containing the generate operation of Metaslang. A side effect of processing such a unit is that the resulting code is written into a 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 transparent to the user. However, it improves the performance and response time of the system.
However, under certain circumstances this may lead to the wrong result. Files only need to be processed if they may have changed since the last time they were processed. To determine whether this is the case, the caching mechanism uses the "last modified" date and time of the files. Say there are two files named mickey.sw and minny.sw. If the user first lets Specware process mickey.sw, and then deletes that file and renames minny.sw to mickey.sw, the system will be fooled into assuming that mickey.sw does not need to be re-processed. After all, its modification time is that of the original minny.sw file, and so it is older than the last time mickey.sw was processed. A likely scenario under which this may happen is when a user copies a file to a back up, modifies the file, has Specware process it, and then restores it by moving the back-up version in its place. All other scenarios that may lead to the wrong results are variations on this theme, replacing a file with one with the same name but different content during a Specware session without adjusting its modification time, or by antedating its modification time.
Clearly, to retain cache integrity, the user is well-advised not to rename, move or delete .sw files while a Specware session is in progress. If there is any reason to suspect that the integrity of the cache has become compromised, the Specware Shell command cinit will clear the unit cache and thereby restore integrity.