What Is A Spec?

In TLA+, the term specification (or spec) is used to mean one of two things:

1. The collection of modules consisting of the root module and and all modules that are imported by the root module, either directly or indirectly, with EXTENDS or INSTANCE statements.  In the context of the Toolbox, we exclude from this collection the standard TLA+ modules such as the Naturals module.  All the specification's module files must be in the same directory as the root module file.
2. The TLA formula that specifies the set of allowed behaviors of the system or algorithm being specified.