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.
We take the word specification by itself to have the first meaning.  We use the term behavior specification when we mean the second.

↑ Managing Your Specifications