¹As explained in Section 7.4.1, specifications can also be given in theories, with a syntax entirely similar to that of modules, but theories, unlike modules, need not be executable.